default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID24th CAV 2012: Berkeley, CA, USA
- P. Madhusudan, Sanjit A. Seshia:
Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science 7358, Springer 2012, ISBN 978-3-642-31423-0
Invited Talks
- Wolfgang Thomas:
Synthesis and Some of Its Challenges. 1 - David L. Dill:
Model Checking Cell Biology. 2
Invited Tutorials
- Rastislav Bodík, Emina Torlak:
Synthesizing Programs with Constraint Solvers. 3 - Aaron R. Bradley:
IC3 and beyond: Incremental, Inductive Verification. 4 - Chris J. Myers
:
Formal Verification of Genetic Circuits. 5 - Michal Moskal:
From C to Infinity and Back: Unbounded Auto-active Verification with VCC. 6
Automata and Synthesis
- Jan Kretínský, Javier Esparza:
Deterministic Automata for the (F, G)-Fragment of LTL. 7-22 - Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný:
Efficient Controller Synthesis for Consumption Games with Multiple Resource Types. 23-38 - Rüdiger Ehlers:
ACTL ∩ LTL Synthesis. 39-54
Inductive Inference and Termination
- Yu-Fang Chen, Bow-Yaw Wang:
Learning Boolean Functions Incrementally. 55-70 - Rahul Sharma, Aditya V. Nori, Alex Aiken:
Interpolants as Classifiers. 71-87 - Wonchan Lee, Bow-Yaw Wang, Kwangkeun Yi:
Termination Analysis with Algorithmic Learning. 88-104 - Marc Brockschmidt, Richard Musiol, Carsten Otto, Jürgen Giesl:
Automated Termination Proofs for Java Programs with Cyclic Data. 105-122 - Javier Esparza, Andreas Gaiser, Stefan Kiefer:
Proving Termination of Probabilistic Programs Using Patterns. 123-138
Abstraction
- Arnaud Venet:
The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. 139-154 - Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger:
Diagnosing Abstraction Failure for Separation Logic-Based Analyses. 155-173 - Aditya V. Thakur, Thomas W. Reps:
A Method for Symbolic Computation of Abstract Operations. 174-192 - Simone Fulvio Rollini, Ondrej Sery, Natasha Sharygina:
Leveraging Interpolant Strength in Model Checking. 193-209
Concurrency and Software Verification
- Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal:
Detecting Fair Non-termination in Multithreaded Programs. 210-226 - Vineet Kahlon, Chao Wang:
Lock Removal for Concurrent Trace Programs. 227-242 - Gerhard Schellhorn, Heike Wehrheim, John Derrick:
How to Prove Algorithms Linearisable. 243-259 - Matthew Hague, Anthony Widjaja Lin:
Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters. 260-276 - Alessandro Cimatti, Alberto Griggio:
Software Model Checking via IC3. 277-293
Biology and Probabilistic Systems
- Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu, Ali Sezgin:
Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits. 294-309 - Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke:
Assume-Guarantee Abstraction Refinement for Probabilistic Systems. 310-326 - Cyrille Jégourel, Axel Legay, Sean Sedwards:
Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking. 327-342
Embedded and Control Systems
- Aditya Zutshi, Sriram Sankaranarayanan, Ashish Tiwari:
Timed Relational Abstractions for Sampled Data Control Systems. 343-361 - Rupak Majumdar, Majid Zamani:
Approximately Bisimilar Symbolic Models for Digital Control Systems. 362-377 - Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, Tiziana Rizzo, Marco Roveri, Angela Sanseviero, Andrei Tchaltsev:
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System. 378-393
SAT/SMT Solving and SMT-based Verification
- Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken:
Minimum Satisfying Assignments for SMT. 394-409 - Cheng-Shen Han, Jie-Hong Roland Jiang:
When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way. 410-426 - Akash Lal, Shaz Qadeer, Shuvendu K. Lahiri:
A Solver for Reachability Modulo Theories. 427-443
Timed and Hybrid Systems
- Shibashis Guha, Chinmay Narayan, S. Arun-Kumar:
On Decidability of Prebisimulation for Timed Automata. 444-461 - Ichiro Hasuo, Kohei Suenaga:
Exercises in Nonstandard Static Analysis of Hybrid Systems. 462-478 - Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski, Martin Wehrle:
A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx. 479-494
Hardware Verification
- Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, Derek Williams:
An Axiomatic Memory Model for POWER Multiprocessors. 495-512 - Flavio M. de Paula, Alan J. Hu, Amir Nahir:
nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces. 513-531 - Zyad Hassan, Aaron R. Bradley, Fabio Somenzi:
Incremental, Inductive CTL Model Checking. 532-547
Security
- Matthew Fredrikson, Richard Joiner, Somesh Jha, Thomas W. Reps, Phillip A. Porras, Hassen Saïdi, Vinod Yegneswaran:
Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement. 548-563 - Boris Köpf, Laurent Mauborgne, Martín Ochoa:
Automatic Quantification of Cache Side-Channels. 564-580 - William R. Harris, Somesh Jha, Thomas W. Reps:
Secure Programming via Visibly Pushdown Safety Games. 581-598
Verification and Synthesis
- Nishant Sinha, Nimit Singhania, Satish Chandra, Manu Sridharan:
Alternate and Learn: Finding Witnesses without Looking All over. 599-615 - Duc-Hiep Chu, Joxan Jaffar:
A Complete Method for Symmetry Reduction in Safety Verification. 616-633 - Rishabh Singh, Sumit Gulwani:
Synthesizing Number Transformations from Input-Output Examples. 634-651
Tool Demonstration Papers
- Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin, Jean-François Raskin:
Acacia+, a Tool for LTL Synthesis. 652-657 - Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl, Alois C. Knoll:
MGSyn: Automatic Synthesis for Industrial Automation. 658-664 - Evan Driscoll, Aditya V. Thakur, Thomas W. Reps:
OpenNWA: A Nested-Word Automaton Library. 665-671 - Aws Albarghouthi, Yi Li, Arie Gurfinkel, Marsha Chechik:
Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. 672-678 - Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina:
SAFARI: SMT-Based Abstraction for Arrays with Interpolants. 679-685 - David Benqué, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex S. Taylor, Moshe Y. Vardi:
Bma: Visual Tool for Modeling and Analyzing Biological Networks. 686-692 - Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell:
APEX: An Analyzer for Open Probabilistic Programs. 693-698 - Philip J. Armstrong, Michael Goldsmith, Gavin Lowe, Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell:
Recent Developments in FDR. 699-704 - Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong:
A Model Checker for Hierarchical Probabilistic Real-Time Systems. 705-711 - Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebêlo:
SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. 712-717 - Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi:
Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. 718-724 - Ashish Tiwari:
HybridSAL Relational Abstracter. 725-731 - Swarat Chaudhuri, Armando Solar-Lezama:
Euler: A System for Numerical Optimization of Programs. 732-737 - Rishabh Singh, Armando Solar-Lezama:
SPT: Storyboard Programming Tool. 738-743 - Patrick Maxim Rondon, Alexander Bakst, Ming Kawaguchi, Ranjit Jhala:
CSolve: Verifying C with Liquid Types. 744-750 - Daniel Schwartz-Narbonne, Feng Liu, David I. August, Sharad Malik:
passert: A Tool for Debugging Parallel Programs. 751-757 - Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa:
TRACER: A Symbolic Execution Tool for Verification. 758-766 - Stephan Arlt, Martin Schäf:
Joogie: Infeasible Code Detection for Java. 767-773 - David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong:
Hector: An Equivalence Checker for a Higher-Order Fragment of ML. 774-780 - Jan Hoffmann, Klaus Aehlig, Martin Hofmann:
Resource Aware ML. 781-786
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-29 02:23 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:
