CAV 2014

57 papers

1. A Conference Management System with Verified Document Confidentiality · Sudeep Kanav, Peter Lammich, Andrei Popescu
2. A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions · Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters
3. A Nonlinear Real Arithmetic Fragment · Ashish Tiwari, Patrick Lincoln
4. A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis · Moritz Sinn, Florian Zuleger, Helmut Veith
5. A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors · Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli
6. AVATAR: The Architecture for First-Order Theorem Provers · Andrei Voronkov
7. An SMT-Based Approach to Coverability Analysis · Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, Filip Niksic
8. Analyzing and Synthesizing Genomic Logic Functions · Nicola Paoletti, Boyan Yordanov, Youssef Hamadi, Christoph M. Wintersteiger, Hillel Kugler
9. Automatic Atomicity Verification for Clients of Concurrent Data Structures · Mohsen Lesani, Todd D. Millstein, Jens Palsberg
10. Automating Separation Logic with Trees and Data · Ruzica Piskac, Thomas Wies, Damien Zufferey
11. Bit-Vector Rewriting with Automatic Rule Generation · Alexander Nadel
12. Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization · Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
13. CEGAR for Qualitative Analysis of Probabilistic Systems · Krishnendu Chatterjee, Martin Chmelik, Przemyslaw Daca
14. Causal Termination of Multi-threaded Programs · Andrey Kupriyanov, Bernd Finkbeiner
15. Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) · Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher
16. Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions · Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun
17. Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion · Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl
18. Engineering a Static Verification Tool for GPU Kernels · Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F. Donaldson + 3 more
19. Finding Instability in Biological Models · Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman
20. From Invariant Checking to Invariant Inference Using Randomized Search · Rahul Sharma, Alex Aiken
21. From LTL to Deterministic Automata: A Safraless Compositional Approach · Javier Esparza, Jan Kretínský
22. G4LTL-ST: Automatic Generation of PLC Programs · Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess, Stefan Stattelmann
23. GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components · Anton Wijs, Joost-Pieter Katoen, Dragan Bosnacki
24. ICE: A Robust Framework for Learning Invariants · Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider
25. Interpolating Property Directed Reachability · Yakir Vizel, Arie Gurfinkel
26. Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells · Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, Marta Z. Kwiatkowska
27. LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes · Alejandro Sánchez, César Sánchez
28. Lazy Annotation Revisited · Kenneth L. McMillan
29. MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications · Petr Cermák, Alessio Lomuscio, Fabio Mogavero, Aniello Murano
30. Minimizing Running Costs in Consumption Systems · Tomás Brázdil, David Klaska, Antonín Kucera, Petr Novotný
31. Monadic Decomposition · Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg
32. Optimal Guard Synthesis for Memory Safety · Thomas Dillig, Isil Dillig, Swarat Chaudhuri
33. Property-Directed Shape Analysis · Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur
34. Proving Non-termination Using Max-SMT · Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
35. QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers · Arlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan
36. Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections · Willem Hagemann
37. Regression Test Selection for Distributed Software Histories · Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov
38. Regression-Free Synthesis for Concurrency · Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach
39. SMACK: Decoupling Source Language Details from Verifier Implementations · Zvonimir Rakamaric, Michael Emmi
40. SMT-Based Model Checking for Recursive Programs · Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
41. Safraless Synthesis for Epistemic Temporal Specifications · Rodica Bozianu, Catalin Dima, Emmanuel Filiot
42. Shape Analysis via Second-Order Bi-Abduction · Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin
43. Software Verification in the Google App-Engine Cloud · Dirk Beyer, Georg Dresler, Philipp Wendler
44. Solving Games without Controllable Predecessor · Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk, Adam Walker
45. String Constraints for Verification · Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer + 1 more
46. Symbolic Resource Bound Inference for Functional Programs · Ravichandhran Madhavan, Viktor Kuncak
47. Symbolic Visibly Pushdown Automata · Loris D'Antoni, Rajeev Alur
48. Synthesis of Masking Countermeasures against Side Channel Attacks · Hassan Eldib, Chao Wang
49. Temporal Mode-Checking for Runtime Monitoring of Privacy Policies · Omar Chowdhury, Limin Jia, Deepak Garg, Anupam Datta
50. Termination Analysis by Learning Terminating Programs · Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
51. The Spirit of Ghost Code · Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
52. The nuXmv Symbolic Model Checker · Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli + 3 more
53. Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction · Suho Lee, Karem A. Sakallah
54. Vac - Verifier of Administrative Role-Based Access Control Policies · Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, Gennaro Parlato
55. Verifying LTL Properties of Hybrid Systems with K-Liveness · Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
56. Verifying Relative Error Bounds Using Symbolic Simulation · Jesse Bingham, Joe Leslie-Hurd
57. Yices 2.2 · Bruno Dutertre