Computer Aided Verification

1. Front Matter

   PDF

2. Software Verification

   1. The Spirit of Ghost Code

      • Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich

      Pages 1-16

   2. SMT-Based Model Checking for Recursive Programs

      • Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki

      Pages 17-34

   3. Property-Directed Shape Analysis

      • Shachar Itzhaky, Nikolaj Bjørner, Thomas Reps, Mooly Sagiv, Aditya Thakur

      Pages 35-51

   4. Shape Analysis via Second-Order Bi-Abduction

      • Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin

      Pages 52-68

   5. ICE: A Robust Framework for Learning Invariants

      • Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider

      Pages 69-87

   6. From Invariant Checking to Invariant Inference Using Randomized Search

      • Rahul Sharma, Alex Aiken

      Pages 88-105

   7. SMACK: Decoupling Source Language Details from Verifier Implementations

      • Zvonimir Rakamarić, Michael Emmi

      Pages 106-113

3. Security

   1. Synthesis of Masking Countermeasures against Side Channel Attacks

      • Hassan Eldib, Chao Wang

      Pages 114-130

   2. Temporal Mode-Checking for Runtime Monitoring of Privacy Policies

      • Omar Chowdhury, Limin Jia, Deepak Garg, Anupam Datta

      Pages 131-149

   3. String Constraints for Verification

      • Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer et al.

      Pages 150-166

   4. A Conference Management System with Verified Document Confidentiality

      • Sudeep Kanav, Peter Lammich, Andrei Popescu

      Pages 167-183

   5. Vac - Verifier of Administrative Role-Based Access Control Policies

      • Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, Gennaro Parlato

      Pages 184-191

4. Automata

   1. From LTL to Deterministic Automata: A Safraless Compositional Approach

      • Javier Esparza, Jan Křetínský

      Pages 192-208

   2. Symbolic Visibly Pushdown Automata

      • Loris D’Antoni, Rajeev Alur

      Pages 209-225

5. Model Checking and Testing

   1. Engineering a Static Verification Tool for GPU Kernels

      • Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F. Donaldson et al.

      Pages 226-242

   2. Lazy Annotation Revisited

      • Kenneth L. McMillan

      Pages 243-259

   3. Interpolating Property Directed Reachability

      • Yakir Vizel, Arie Gurfinkel

      Pages 260-276

   4. Verifying Relative Error Bounds Using Symbolic Simulation

      • Jesse Bingham, Joe Leslie-Hurd

      Pages 277-292

   5. Regression Test Selection for Distributed Software Histories

      • Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov

      Pages 293-309

This book constitutes the proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 46 regular papers and 11 short papers presented in this volume were carefully reviewed and selected from a total of 175 regular and 54 short paper submissions. The contributions are organized in topical sections named: software verification; automata; model checking and testing; biology and hybrid systems; games and synthesis; concurrency; SMT and theorem proving; bounds and termination; and abstraction.

• artificial intelligence
• concurrency
• formal languages and automata theory
• formal methods
• formal methods and theory of security
• formal software verification
• hardware verification and validation
• logic
• logic and verification
• model checking
• program reasoning
• semantics and reasoning
• software engineering
• software functional properties
• software verification and validation
• solvers
• theorem proving
• verification by model checking

• Johannes Kepler University Linz, Linz, Austria

  Armin Biere

• IAIK, Graz University of Technology, Graz, Austria

  Roderick Bloem

Policies and ethics