Abstract

We present an approach for the combination of techniques from model checking and static analysis for the verification of reactive systems. These systems appear in various forms, e.g. as Web services, decision support systems, or logic controllers. Reactive systems are characterized by nonterminating or infinite executions. Executions start from some initial state and then continue forever, while possibly receiving stimulus from some external environment. Our analyzed systems range from structurally simple to structurally complex systems. We address the verification of reachability properties and behavioral program properties. Reachability properties are represented by assertions in the program and we determine statically whether an assertion holds for all (infinite) execution paths. Behavioral properties are represented as linear temporal logic formulae specifying the input/output behavior of the program. For improved performance we also dispatch parts of the program analysis to the linked transformed binary version of the analyzed program. All analyses are run in parallel and we present results for scaling on multi-core machines. Various parameters are used to tune the precision of the combined analyses, and thus, the number of successfully verified (or falsified) program properties. As benchmarks we use the C benchmarks from the RERS Challenges 2012-2014.

Biography

Markus Schordan joined the Center for Applied Scientific Computing (CASC) at Lawrence Livermore National Laboratory, CA, USA, in April 2013 as a senior computer scientist. His research interests include program analysis and verification, programming languages for high-performance computing, and compiler construction. He previously held positions at University Klagenfurt (1997-2001), Lawrence Livermore National Laboratory (2001-2003 (Post-Doc)), TU Vienna (2003-2008), and UAS Technikum Wien (2008-2013). In 2009 he received an R&D 100 AWARD (ROSE), in 2011 a Best Paper Award at the 11th IEEE Source-Code and Manipulation Conference (SCAM 2011), and in 2012 and 2013 the Method Combination Award in the RERS Challenges.

He received a Diploma Degree in computer science from TU Vienna in 1997, and a PhD degree from University Klagenfurt in 2001 (with distinction). He is author or co-author of 30+ refereed and invited papers of conferences and journals.

Note

This talk is organized by the Compilers and Languages Group at the Institute of Computer Languages. Tea at the library of E185/1, Argentinierstr. 8, 4th floor (central) at 13:30.

Speakers

• Dr. Markus Schordan, Lawrence Livermore National Laboratory, CA, USA

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.

Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!