default search action
26th CAV 2014: Vienna, Austria
- Armin Biere, Roderick Bloem
:
Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science 8559, Springer 2014, ISBN 978-3-319-08866-2
Software Verification
- Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich:
The Spirit of Ghost Code. 1-16 - Anvesh Komuravelli, Arie Gurfinkel
SMT-Based Model Checking for Recursive Programs. 17-34 - Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur:
Property-Directed Shape Analysis. 35-51 - Quang Loc Le, Cristian Gherghina, Shengchao Qin
Shape Analysis via Second-Order Bi-Abduction. 52-68 - Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider
ICE: A Robust Framework for Learning Invariants. 69-87 - Rahul Sharma, Alex Aiken:
From Invariant Checking to Invariant Inference Using Randomized Search. 88-105 - Zvonimir Rakamaric, Michael Emmi:
SMACK: Decoupling Source Language Details from Verifier Implementations. 106-113
Security
- Hassan Eldib, Chao Wang:
Synthesis of Masking Countermeasures against Side Channel Attacks. 114-130 - Omar Chowdhury, Limin Jia
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies. 131-149 - Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen
String Constraints for Verification. 150-166 - Sudeep Kanav, Peter Lammich
A Conference Management System with Verified Document Confidentiality. 167-183 - Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, Gennaro Parlato
Vac - Verifier of Administrative Role-Based Access Control Policies. 184-191
Automata
- Javier Esparza
From LTL to Deterministic Automata: A Safraless Compositional Approach. 192-208 - Loris D'Antoni, Rajeev Alur:
Symbolic Visibly Pushdown Automata. 209-225
Model Checking and Testing
- Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis
Engineering a Static Verification Tool for GPU Kernels. 226-242 - Kenneth L. McMillan:
Lazy Annotation Revisited. 243-259 - Yakir Vizel, Arie Gurfinkel
Interpolating Property Directed Reachability. 260-276 - Jesse Bingham, Joe Leslie-Hurd:
Verifying Relative Error Bounds Using Symbolic Simulation. 277-292 - Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov:
Regression Test Selection for Distributed Software Histories. 293-309 - Anton Wijs
GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components. 310-326 - Dirk Beyer
Software Verification in the Google App-Engine Cloud. 327-333 - Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio
The nuXmv Symbolic Model Checker. 334-342
Biology and Hybrid Systems
- Nicola Paoletti
Analyzing and Synthesizing Genomic Logic Functions. 343-357 - Byron Cook, Jasmin Fisher
Finding Instability in Biological Models. 358-372 - Zhenqi Huang, Chuchu Fan
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells. 373-390 - Henri Hansen
Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions. 391-406 - Willem Hagemann:
Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections. 407-423 - Alessandro Cimatti
Verifying LTL Properties of Hybrid Systems with K-Liveness. 424-440
Games and Synthesis
- Rodica Bozianu, Catalin Dima, Emmanuel Filiot:
Safraless Synthesis for Epistemic Temporal Specifications. 441-456 - Tomás Brázdil, David Klaska, Antonín Kucera, Petr Novotný
Minimizing Running Costs in Consumption Systems. 457-472 - Krishnendu Chatterjee, Martin Chmelik, Przemyslaw Daca:
CEGAR for Qualitative Analysis of Probabilistic Systems. 473-490 - Thomas Dillig, Isil Dillig, Swarat Chaudhuri:
Optimal Guard Synthesis for Memory Safety. 491-507 - Jade Alglave, Daniel Kroening
Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion. 508-524 - Petr Cermák, Alessio Lomuscio
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications. 525-532 - Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk, Adam Walker:
Solving Games without Controllable Predecessor. 533-540 - Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess, Stefan Stattelmann:
G4LTL-ST: Automatic Generation of PLC Programs. 541-549
Concurrency
- Mohsen Lesani, Todd D. Millstein
Automatic Atomicity Verification for Clients of Concurrent Data Structures. 550-567 - Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach:
Regression-Free Synthesis for Concurrency. 568-584 - Omar Inverso
Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. 585-602 - Javier Esparza
An SMT-Based Approach to Coverability Analysis. 603-619 - Alejandro Sánchez, César Sánchez
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes. 620-627
SMT and Theorem Proving
- Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg:
Monadic Decomposition. 628-645 - Tianyi Liang, Andrew Reynolds, Cesare Tinelli
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. 646-662 - Alexander Nadel
Bit-Vector Rewriting with Automatic Rule Generation. 663-679 - Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. 680-695 - Andrei Voronkov:
AVATAR: The Architecture for First-Order Theorem Provers. 696-710 - Ruzica Piskac
Automating Separation Logic with Trees and Data. 711-728 - Ashish Tiwari, Patrick Lincoln:
A Nonlinear Real Arithmetic Fragment. 729-736 - Bruno Dutertre:
Yices 2.2. 737-744
Bounds and Termination
- Moritz Sinn, Florian Zuleger, Helmut Veith:
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. 745-761 - Ravichandhran Madhavan
Symbolic Resource Bound Inference for Functional Programs. 762-778 - Daniel Larraz
Proving Non-termination Using Max-SMT. 779-796 - Matthias Heizmann
Termination Analysis by Learning Terminating Programs. 797-813 - Andrey Kupriyanov, Bernd Finkbeiner:
Causal Termination of Multi-threaded Programs. 814-830
Abstraction
- Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). 831-848 - Suho Lee, Karem A. Sakallah:
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction. 849-865 - Arlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan:
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. 866-873
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-15 01:31 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: