default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID25th CAV 2013: Saint Petersburg, Russia
- Natasha Sharygina
, Helmut Veith:
Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science 8044, Springer 2013, ISBN 978-3-642-39798-1
Invited Tutorials
- Laura Kovács, Andrei Voronkov:
First-Order Theorem Proving and Vampire. 1-35 - Matthias Heizmann, Jochen Hoenicke, Andreas Podelski:
Software Model Checking for People Who Love Automata. 36-52 - Hristina Palikareva, Cristian Cadar:
Multi-solver Support in Symbolic Execution. 53-68
Biology
- Loïc Paulevé, Geoffroy Andrieux, Heinz Koeppl:
Under-Approximating Cut Sets for Reachability in Large Scale Automata Networks. 69-84 - Koen Claessen, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Qinsi Wang:
Model-Checking Signal Transduction Networks through Decreasing Reachability Sets. 85-100 - Johannes G. Reiter, Ivana Bozic, Krishnendu Chatterjee, Martin A. Nowak:
TTP: Tool for Tumor Progression. 101-106 - Lubos Brim, Milan Ceska, Sven Drazan, David Safránek:
Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. 107-123
Concurrency
- Javier Esparza, Pierre Ganty, Rupak Majumdar:
Parameterized Verification of Asynchronous Shared-Memory Systems. 124-140 - Jade Alglave, Daniel Kroening, Michael Tautschnig:
Partial Orders for Efficient Bounded Model Checking of Concurrent Software. 141-157 - Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac:
Incremental, Inductive Coverability. 158-173 - Cezara Dragoi, Ashutosh Gupta, Thomas A. Henzinger:
Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. 174-190 - Azadeh Farzan, Zachary Kincaid:
Duet: Static Analysis for Unbounded Parallelism. 191-196
Hardware
- Roy Armoni, Dana Fisman, Naiyong Jin:
SVA and PSL Local Variables - A Practical Approach. 197-212 - Thomas Braibant, Adam Chlipala:
Formal Verification of Hardware Synthesis. 213-228 - Guanfeng Lv, Kaile Su, Yanyan Xu:
CacBDD: A BDD Package with Dynamic Cache Management. 229-234 - Brad D. Bingham, Jesse D. Bingham, John Erickson, Mark R. Greenstreet:
Distributed Explicit State Model Checking of Deadlock Freedom. 235-241
Hybrid Systems
- Hui Kong, Fei He, Xiaoyu Song, William N. N. Hung, Ming Gu:
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems. 242-257 - Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan:
Flow*: An Analyzer for Non-linear Hybrid Systems. 258-263 - Alexandre Donzé, Thomas Ferrère, Oded Maler:
Efficient Robust Monitoring for STL. 264-279 - Pavithra Prabhakar, Miriam Garcia Soto:
Abstraction Based Model-Checking of Stability of Hybrid Systems. 280-295 - Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Fabio Merli, Enrico Tronci:
System Level Formal Verification via Model Checking Driven Simulation. 296-312
Interpolation
- Aws Albarghouthi, Kenneth L. McMillan:
Beautiful Interpolants. 313-329 - Yakir Vizel, Vadim Ryvchin, Alexander Nadel:
Efficient Generation of Small Interpolants in CNF. 330-346 - Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
Disjunctive Interpolants for Horn-Clause Verification. 347-363 - Liyun Dai, Bican Xia, Naijun Zhan:
Generating Non-linear Interpolants by Semidefinite Programming. 364-380
Loops and Termination
- Daniel Kroening, Matt Lewis, Georg Weissenbacher:
Under-Approximating Loops in C Programs for Fast Counterexample Detection. 381-396 - Pierre Ganty, Samir Genaim:
Proving Termination Starting from the End. 397-412 - Marc Brockschmidt, Byron Cook, Carsten Fuhs:
Better Termination Proving through Cooperation. 413-429
New Domains
- Oshri Adler, Cindy Eisner, Tatyana Veksler:
Relative Equivalence in the Presence of Ambiguity. 430-446 - Arun Tejasvi Chaganty, Akash Lal, Aditya V. Nori, Sriram K. Rajamani:
Combining Relational Learning with SMT Solvers Using CEGAR. 447-462 - Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus:
A Fully Verified Executable LTL Model Checker. 463-478 - Shaull Almagor, Guy Avni, Orna Kupferman:
Automatic Generation of Quality Specifications. 479-494
Probability and Statistics
- Alistair Stewart, Kousha Etessami, Mihalis Yannakakis:
Upper Bounds for Newton's Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata. 495-510 - Aleksandar Chakarov, Sriram Sankaranarayanan:
Probabilistic Program Analysis with Martingales. 511-526 - Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia:
Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. 527-542 - Krishnendu Chatterjee, Jakub Lacki:
Faster Algorithms for Markov Decision Processes with Low Treewidth. 543-558 - Krishnendu Chatterjee, Andreas Gaiser, Jan Kretínský:
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. 559-575 - Cyrille Jégourel, Axel Legay, Sean Sedwards:
Importance Splitting for Statistical Model Checking Rare Properties. 576-591
SAT and SMT
- João Marques-Silva, Mikolás Janota, Anton Belov:
Minimal Sets over Monotone Predicates in Boolean Formulae. 592-607 - Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi:
A Scalable and Nearly Uniform Generator of SAT Witnesses. 608-623 - Loris D'Antoni, Margus Veanes:
Equivalence of Extended Symbolic Finite Transducers. 624-639 - Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic:
Finite Model Finding in SMT. 640-655 - Chih-Hong Cheng, Harald Ruess, Natarajan Shankar:
JBernstein: A Validity Checker for Generalized Polynomial Constraints. 656-661 - Panagiotis Manolios, Vasilis Papavasileiou:
ILP Modulo Theories. 662-677 - Richard Uhler, Nirav Dave:
Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries. 678-683 - Isil Dillig, Thomas Dillig:
Explain: A Tool for Performing Abductive Inference. 684-689
Security
- Tom Chothia, Yusuke Kawamoto, Chris Novakovic:
A Tool for Estimating Information Leakage. 690-695 - Simon Meier, Benedikt Schmidt, Cas Cremers, David A. Basin:
The TAMARIN Prover for the Symbolic Analysis of Security Protocols. 696-701 - Fabrizio Biondi, Axel Legay, Louis-Marie Traonouez, Andrzej Wasowski:
QUAIL: A Quantitative Security Analyzer for Imperative Code. 702-707 - Vincent Cheval, Véronique Cortier, Antoine Plet:
Lengths May Break Privacy - Or How to Check for Equivalences with Length. 708-723 - Adi Sosnovich, Orna Grumberg, Gabi Nakibly:
Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems. 724-739
Shape Analysis
- Lukás Holík, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar:
Fully Automated Shape Analysis Based on Forest Automata. 740-755 - Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv:
Effectively-Propositional Reasoning about Reachability in Linked Data Structures. 756-772 - Ruzica Piskac, Thomas Wies, Damien Zufferey:
Automating Separation Logic Using SMT. 773-789 - Christoph Haase, Samin Ishtiaq, Joël Ouaknine, Matthew J. Parkinson:
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. 790-795
Software Verification
- William R. Harris, Guoliang Jin, Shan Lu, Somesh Jha:
Validating Library Usage Interactively. 796-812 - Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider:
Learning Universally Quantified Invariants of Linear Data Structures. 813-829 - Maximilien Colange, Souheib Baarir, Fabrice Kordon, Yann Thierry-Mieg:
Towards Distributed Software Model-Checking Using Decision Diagrams. 830-845 - Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke:
Automatic Abstraction in SMT-Based Unbounded Software Model Checking. 846-862 - Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlícek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimír Still, Jirí Weiser:
DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. 863-868 - Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko:
Solving Existentially Quantified Horn Clauses. 869-882
Synthesis
- Ming-Hsien Tsai, Yih-Kuen Tsay, Yu-Shiang Hwang:
GOAL for Games, Omega-Automata, and Logics. 883-889 - Romain Brenguier:
PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games. 890-895 - Christian von Essen, Barbara Jobstmann:
Program Repair without Regret. 896-911 - Daniel Wonisch, Alexander Schremmer, Heike Wehrheim:
Programs from Proofs - A PCC Alternative. 912-927 - Ayrat Khalimov, Swen Jacobs, Roderick Bloem:
PARTY Parameterized Synthesis of Token Rings. 928-933 - Aws Albarghouthi, Sumit Gulwani, Zachary Kincaid:
Recursive Program Synthesis. 934-950 - Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach:
Efficient Synthesis for Concurrency by Semantics-Preserving Transformations. 951-967
Time
- Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, Jaco van de Pol:
Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction. 968-983 - Étienne André, Yang Liu, Jun Sun, Jin Song Dong, Shang-Wei Lin:
PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. 984-989 - Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz:
Lazy Abstractions for Timed Automata. 990-1005 - Ocan Sankur:
Shrinktech: A Tool for the Robustness Analysis of Timed Automata. 1006-1012
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:
