default search action
14th FMCAD 2014: Lausanne, Switzerland
- Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014. IEEE 2014, ISBN 978-0-9835678-4-4
Tutorials
- Ziyad Hanna:
Challenging problems in industrial formal verification. 1 - Armin Biere:
Challenges in bit-precise reasoning. 3 - Johannes Kinder:
Efficient symbolic execution for software testing. 5 - Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli:
A tour of CVC4: How it works, and how to use it. 7
Invited Talks and Student Forum
- Xavier Leroy:
Compiler verification for fun and profit. 9 - Thomas A. Henzinger:
Computer-aided verification technology for biology. 11 - Ruzica Piskac:
The FMCAD 2014 graduate student forum. 13
Contributed Articles
- Brad D. Bingham, Mark R. Greenstreet:
Response property checking via distributed state space exploration. 15-22 - Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario, Alberto Griggio:
Towards Pareto-optimal parameter synthesis for monotonic cost functions. 23-30 - Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing:
SAT-based methods for circuit synthesis. 31-34 - Roderick Bloem, Georg Hofferek, Bettina Könighofer, Robert Könighofer, Simon Ausserlechner, Raphael Spork:
Synthesis of synchronization using uninterpreted functions. 35-42 - Gianpiero Cabodi, Marco Palena, Paolo Pasini:
Interpolation with Guided Refinement: Revisiting incrementality in SAT-based unbounded model checking. 43-50 - Sagar Chaki, Arie Gurfinkel, Nishant Sinha:
Efficient verification of periodic programs using sequential consistency and snapshots. 51-58 - Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám:
Under-approximate flowpipes for non-linear continuous systems. 59-66 - Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn:
Disproving termination with overapproximation. 67-74 - Byron Cook, Heidy Khlaaf, Nir Piterman:
Faster temporal reasoning for infinite-state programs. 75-82 - Adrià Gascón, Pramod Subramanyan, Bruno Dutertre, Ashish Tiwari, Dejan Jovanovic, Sharad Malik:
Template-based circuit understanding. 83-90 - Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh:
Simulation and formal verification of x86 machine-code programs that make system calls. 91-98 - Arie Gurfinkel, Yakir Vizel:
DRUPing for interpolates. 99-106 - Marijn Heule, Martina Seidl, Armin Biere:
Efficient extraction of Skolem functions from QRAT proofs. 107-114 - Alexander Ivrii, Arie Gurfinkel, Anton Belov:
Small inductive safe invariants. 115-122 - Pavel Jancík, Jan Kofron, Simone Fulvio Rollini, Natasha Sharygina:
On interpolants and variable assignments. 123-130 - Daher Kaiss, Jonathan Kalechstain:
Post-silicon timing diagnosis made simple using formal technology. 131-138 - Tim King, Clark W. Barrett, Cesare Tinelli:
Leveraging linear and mixed integer programming for SMT. 139-146 - Akash Lal, Shaz Qadeer:
A program transformation for faster goal-directed search. 147-154 - Peizun Liu, Thomas Wahl:
Infinite-state backward exploration of Boolean broadcast programs. 155-162 - Rupak Majumdar, Sai Deep Tetali, Zilong Wang:
Kuai: A model checker for software-defined networks. 163-170 - Panagiotis Manolios, Vasilis Papavasileiou, Mirek Riedewald:
ILP Modulo Data. 171-178 - Aina Niemetz, Mathias Preiner, Armin Biere:
Turbo-charging Lemmas on demand with don't care reasoning. 179-186 - Corneliu Popeea, Andrey Rybalchenko, Andreas Wilhelm:
Reduction for compositional verification of multi-threaded programs. 187-194 - Andrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura:
Finding conflicting instances of quantified formulas in SMT. 195-202 - Karsten Scheibler, Bernd Becker:
Using interval constraint propagation for pseudo-Boolean constraint solving. 203-206 - Enrico Tronci, Toni Mancini, Ivano Salvo, Stefano Sinisi, Federico Mari, Igor Melatti, Annalisa Massini, Francesco Davì, Thomas Dierkes, Rainald Ehrig, Susanna Röblitz, Brigitte Leeners, Tillmann H. C. Kruger, Marcel Egli, Fabian Ille:
Patient-specific models from inter-patient biological models and clinical records. 207-214 - Amirhossein Vakili, Nancy A. Day:
Reducing CTL-live model checking to first-order logic validity checking. 215-218 - Adam Walker, Leonid Ryzhyk:
Predicate abstraction for reactive synthesis. 219-226
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.