default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID29th CAV 2017: Heidelberg, Germany
- Rupak Majumdar, Viktor Kuncak:
Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Lecture Notes in Computer Science 10427, Springer 2017, ISBN 978-3-319-63389-3
Analysis of Software and Hardware
- Matthew Amy, Martin Roetteler
, Krysta M. Svore:
Verified Compilation of Space-Efficient Reversible Circuits. 3-21 - Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke:
Ascertaining Uncertainty for Efficient Exact Cache Analysis. 22-40 - Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady:
Non-polynomial Worst-Case Analysis of Recursive Programs. 41-63 - Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao:
Automated Resource Analysis with Coq Proof Objects. 64-85 - Adrià Gascón, Ashish Tiwari, Brent Carmer, Umang Mathur:
Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis. 86-103 - Eshan Singh, Clark W. Barrett, Subhasish Mitra:
E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods. 104-125 - Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett:
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. 126-133
Foundations of Verification
- John Fearnley:
Efficient Parallel Strategy Improvement for Parity Games. 137-154 - Marie Fortin, Anca Muscholl, Igor Walukiewicz:
Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems. 155-175 - Olli Saarikivi, Margus Veanes:
Minimization of Symbolic Transducers. 176-196 - Marcelo Sousa, César Rodríguez, Vijay Victor D'Silva, Daniel Kroening:
Abstract Interpretation with Unfoldings. 197-216 - Ognjen Maric, Christoph Sprenger, David A. Basin:
Cutoff Bounds for Consensus Algorithms. 217-237 - Paul Beame, Vincent Liew:
Towards Verifying Nonlinear Integer Arithmetic. 238-258
Distributed and Networked Systems
- Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, Martin T. Vechev:
Network-Wide Configuration Synthesis. 261-281 - Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv:
Verifying Equivalence of Spark Programs. 282-300 - Jedidiah McClurg, Hossein Hojjat, Pavol Cerný:
Synchronization Synthesis for Network Programs. 301-321
Synthesis
- Peter Faymonville, Bernd Finkbeiner, Leander Tentrup:
BoSy: An Experimentation Framework for Bounded Synthesis. 325-332 - Ayrat Khalimov, Roderick Bloem:
Bounded Synthesis for Streett, Rabin, and \text CTL^*. 333-352 - Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, Yaron Velner:
Quantitative Assume Guarantee Synthesis. 353-374 - Luca Cardelli, Milan Ceska, Martin Fränzle, Marta Z. Kwiatkowska, Luca Laurenti, Nicola Paoletti, Max Whitby:
Syntax-Guided Optimal Synthesis for Chemical Reaction Networks. 375-395
Decision Procedures and Their Applications
- Minh-Thai Trinh, Duc-Hiep Chu, Joxan Jaffar:
Model Counting for Recursively-Defined Strings. 399-418 - Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex:
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. 419-435 - Alexander Nadel:
A Correct-by-Decision Solution for Simultaneous Place and Route. 436-452 - Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli:
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. 453-474 - Leander Tentrup:
On Expansion and Resolution in CEGAR Based QBF Solving. 475-494 - Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin:
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. 495-517
Software Analysis
- Andrei Marian Dan, Manu Sridharan, Satish Chandra, Jean-Baptiste Jeannin, Martin T. Vechev:
Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts. 521-541 - Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil:
Proving Linearizability Using Forward Simulations. 542-563 - Bernd Finkbeiner, Christopher Hahn, Marvin Stenger:
EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties. 564-570 - Hiroshi Unno, Sho Torii, Hiroki Sakamoto:
Automating Induction for Solving Horn Clauses. 571-591 - Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk:
A Storm is Coming: A Modern Probabilistic Model Checker. 592-600 - Amir M. Ben-Amram, Samir Genaim:
On Multiphase-Linear Ranking Functions. 601-620
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 2025-11-04 22:22 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:
