default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID26th 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, Sagar Chaki:
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, Wei-Ngan Chin:
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, Deepak Garg, Anupam Datta:
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies. 131-149 - Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman:
String Constraints for Verification. 150-166 - Sudeep Kanav, Peter Lammich, Andrei Popescu:
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, Jan Kretínský:
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, Alastair F. Donaldson, Jeroen Ketema, Daniel Liew, Shaz Qadeer:
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, Joost-Pieter Katoen, Dragan Bosnacki:
GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components. 310-326 - Dirk Beyer, Georg Dresler, Philipp Wendler:
Software Verification in the Google App-Engine Cloud. 327-333 - Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta:
The nuXmv Symbolic Model Checker. 334-342
Biology and Hybrid Systems
- Nicola Paoletti, Boyan Yordanov, Youssef Hamadi, Christoph M. Wintersteiger, Hillel Kugler:
Analyzing and Synthesizing Genomic Logic Functions. 343-357 - Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman:
Finding Instability in Biological Models. 358-372 - Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, Marta Z. Kwiatkowska:
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells. 373-390 - Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun:
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, Alberto Griggio, Sergio Mover, Stefano Tonetta:
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, Vincent Nimal, Daniel Poetzl:
Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion. 508-524 - Petr Cermák, Alessio Lomuscio, Fabio Mogavero, Aniello Murano:
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, Jens Palsberg:
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, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato:
Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. 585-602 - Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, Filip Niksic:
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, Clark W. Barrett, Morgan Deters:
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, Cesare Tinelli:
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, Thomas Wies, Damien Zufferey:
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, Viktor Kuncak:
Symbolic Resource Bound Inference for Functional Programs. 762-778 - Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Proving Non-termination Using Max-SMT. 779-796 - Matthias Heizmann, Jochen Hoenicke, Andreas Podelski:
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 2026-01-27 23:58 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:
