21. CADE 2007: Bremen, Germany - VERIFY

Abstracts of Invited Talks

• Tobias Nipkow:
  Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic.
  
• Aaron Stump:
  Lightweight Verification with Dependent Types.
  
• Cesare Tinelli:
  Trends and Challenges in Satisfiability Modulo Theories.
  

Research Papers

• Eyad Alkassar, Mark A. Hillebrand, Steffen Knapp, Rostislav Rusev, Sergey Tverdyshev:
  Formal Device and Programming Model for a Serial Interface.
  
• Mamoun Filali:
  A Mechanization of Phylogenetic Trees.
  
• Pascal Fontaine:
  Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class.
  
• Borislav Gajanovic, Bernhard Rumpe:
  ALICE: An Advanced Logic for Interactive Component Engineering.
  
• Bruno Langenstein, Andreas Nonnengart, Georg Rock, Werner Stephan:
  A History-based Verification of Distributed Applications.
  
• Daniel Larsson, Reiner Hähnle:
  Symbolic Fault Injection.
  
• Jia Meng, Lawrence C. Paulson, Gerwin Klein:
  A Termination Checker for Isabelle Hoare Logic.
  
• Till Mossakowski, Christian Maeder, Klaus Lüttich:
  The Heterogeneous Tool Set (Hets).
  
• Wojciech Mostowski:
  Fully Verified Java Card API Reference Implementation.
  
• Olivera Pavlovic, Ralf Pinger, Maik Kollmann:
  Automation of Formal Verification of PLC Programs Written in IL.
  
• André Platzer:
  Combining Deduction and Algebraic Constraints for Hybrid System Analysis.
  
• Philipp Rümmer:
  A Sequent Calculus for Integer Arithmetic with Counterexample Generation.
  
• Peter H. Schmitt, Benjamin Weiß:
  Inferring Invariants by Symbolic Execution.