Institute of Computer Languages
Compilers and Languages Group

Talks 2014 - Dr. Markus Schordan

Der Arbeitsbereich für Programmiersprachen und Übersetzer am Institut für Computersprachen lädt zu folgendem Vortrag ein:

Dr. Markus Schordan

Lawrence Livermore National Laboratory, CA, USA

über

Combination of Static Analysis and Model Checking Techniques for Scalable Verification

Datum: Freitag, den 3. Oktober 2014
Zeit: 14:00 Uhr c.t. *)
Ort: TU Wien, Seminarraum Argentinierstr. 8 (Erdgeschoss)
*) Tee: 13:30 Uhr in der Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).

Zusammenfassung:

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.

Kurzbiographie

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. ( http://people.llnl.gov/schordan1 )

Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.

Complang
   About Us
   Research
   Lehre
   Service
      Robotics
      Library
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Sitemap
Contact
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)