Sciweavers

CAV
2009
Springer
184views Hardware» more  CAV 2009»
15 years 2 days ago
Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
Abstract. We present a new technique called Monotonic Partial Order Reduction (MPOR) that effectively combines dynamic partial order reduction with symbolic state space exploration...
Vineet Kahlon, Chao Wang, Aarti Gupta
CAV
2009
Springer
135views Hardware» more  CAV 2009»
15 years 2 days ago
Sliding Window Abstraction for Infinite Markov Chains
Window Abstraction for Infinite Markov Chains Thomas A. Henzinger1 , Maria Mateescu1 , and Verena Wolf1,2 1 EPFL, Switzerland 2 Saarland University, Germany Abstract. We present an...
Thomas A. Henzinger, Maria Mateescu, Verena Wolf
CAV
2009
Springer
137views Hardware» more  CAV 2009»
15 years 2 days ago
An Antichain Algorithm for LTL Realizability
Emmanuel Filiot, Jean-François Raskin, Naiy...
CAV
2009
Springer
169views Hardware» more  CAV 2009»
15 years 2 days ago
Automatic Verification of Integer Array Programs
We provide a verification technique for a class of programs working on integer arrays of finite, but not a priori bounded length. We use the logic of integer arrays SIL [13] to spe...
Filip Konecný, Marius Bozga, Peter Habermeh...
CAV
2009
Springer
187views Hardware» more  CAV 2009»
15 years 2 days ago
A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints
We describe a Markov chain Monte Carlo (MCMC)-based algorithm for sampling solutions to mixed Boolean/integer constraint problems. The focus of this work differs in two points from...
Nathan Kitchen, Andreas Kuehlmann
CAV
2009
Springer
139views Hardware» more  CAV 2009»
15 years 2 days ago
A Concurrent Portfolio Approach to SMT Solving
With the availability of multi-core processors and large-scale computing clusters, the study of parallel algorithms has been revived throughout the industry. We present a portfolio...
Christoph M. Wintersteiger, Leonardo Mendonç...
CAV
2009
Springer
181views Hardware» more  CAV 2009»
15 years 2 days ago
Size-Change Termination, Monotonicity Constraints and Ranking Functions
Abstract. Size-change termination involves deducing program termination based on the impossibility of infinite descent. To this end we may use m abstraction in which transitions ar...
Amir M. Ben-Amram