Sciweavers

CAV
2007
Springer
212views Hardware» more  CAV 2007»
13 years 8 months ago
A Tutorial on Satisfiability Modulo Theories
Abstract. Solvers for satisfiability modulo theories (SMT) check the satisfiability of first-order formulas containing operations from various theories such as the Booleans, bit-ve...
Leonardo Mendonça de Moura, Bruno Dutertre,...
CAV
2007
Springer
121views Hardware» more  CAV 2007»
13 years 8 months ago
Automated Assumption Generation for Compositional Verification
Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu
CAV
2007
Springer
111views Hardware» more  CAV 2007»
13 years 8 months ago
Verification Across Intellectual Property Boundaries
In many industries, the share of software components provided by third-party suppliers is steadily increasing. As the suppliers seek to secure their intellectual property (IP) righ...
Sagar Chaki, Christian Schallhart, Helmut Veith
CAV
2007
Springer
112views Hardware» more  CAV 2007»
13 years 8 months ago
Structural Abstraction of Software Verification Conditions
al Abstraction of Software Verification Conditions Domagoj Babi
Domagoj Babic, Alan J. Hu
CAV
2007
Springer
117views Hardware» more  CAV 2007»
13 years 8 months ago
Spade: Verification of Multithreaded Dynamic and Recursive Programs
Gaël Patin, Mihaela Sighireanu, Tayssir Touil...
CAV
2007
Springer
145views Hardware» more  CAV 2007»
13 years 8 months ago
Hybrid Systems: From Verification to Falsification
We propose HyDICE, Hybrid DIscrete Continuous Exploration, a multi-layered approach for hybrid-system testing that integrates continuous sampling-based robot motion planning with d...
Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi
CAV
2007
Springer
108views Hardware» more  CAV 2007»
13 years 8 months ago
Parametric and Sliced Causality
Abstract. Happen-before causal partial orders have been widely used in concurrent program verification and testing. This paper presents a parametric approach to happen-before causa...
Feng Chen, Grigore Rosu
CAV
2007
Springer
227views Hardware» more  CAV 2007»
13 years 8 months ago
The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems
Abstract. In this paper, we describe the features of the Timed Abstract State Machine toolset. The toolset implements the features of the Timed Abstract State Machine (TASM) langua...
Martin Ouimet, Kristina Lundqvist
CAV
2007
Springer
114views Hardware» more  CAV 2007»
13 years 8 months ago
Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concern...
Dirk Beyer, Thomas A. Henzinger, Grégory Th...