


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.