Volume 144,
Number 1,
January 2006
Proceedings of the Third International Workshop on Bounded Model Checking (BMC 2005)
- Armin Biere, Ofer Strichman:
Preface.
1-
- Markus Jehle, Jan Johannsen, Martin Lange, Nicolas Rachinsky:
Bounded Model Checking for All Regular Properties.
3-18
- Anders Franzén:
Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs.
19-33
- Ohad Shacham, Karen Yorav:
Adaptive Application of SAT Solving Techniques.
35-50
- Mohammad Awedh, Fabio Somenzi:
Termination Criteria for Bounded Model Checking: Extensions and Comparison.
51-66
- Daniel Geist, Mark Ginzburg, Yoad Lustig, Ishai Rabinovitz, Ohad Shacham, Rachel Tzoref:
Supporting SAT based BMC on Finite Path Models.
67-77
- Daniel Kroening:
Computing Over-Approximations with Bounded Model Checking.
79-92
Volume 144,
Number 2,
January 2006
Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005)
- Alessandro Armando, Alessandro Cimatti:
Preface.
1-2
- Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani:
Encoding RTL Constructs for MathSAT: a Preliminary Report.
3-14
- Jim Grundy, Thomas F. Melham, Sava Krstic, Sean McLaughlin:
Tool Building Requirements for an API to First-Order Solvers.
15-26
- Shuvendu K. Lahiri, Madanlal Musuvathi:
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals.
27-41
- Sean McLaughlin, Clark Barrett, Yeting Ge:
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite.
43-51
- Amir Pnueli, Ofer Strichman:
Reduced Functional Consistency of Uninterpreted Functions.
53-65
- Tjark Weber:
Integrating a SAT Solver with an LCF-style Theorem Prover.
67-78
- Ian Wehrman, Aaron Stump:
Mining Propositional Simplification Proofs for Small Validating Clauses.
79-91
Volume 144,
Number 3,
February 2006
Proceedings of the Workshop on Software Model Checking (SoftMC 2005)
- Byron Cook, Scott D. Stoller, Willem Visser:
Preface.
1-2
- Wolfgang Grieskamp, Nikolai Tillmann, Wolfram Schulte:
XRT- Exploring Runtime for .NET Architecture and Applications.
3-26
- Radu Grosu, Xiaowan Huang, Sumit Jain, Scott A. Smolka:
Open-Source Model Checking.
27-44
- Graham Hughes, Sreeranga P. Rajan, Tom Sidle, Keith Swenson:
Error Detection in Concurrent Java Programs.
45-58
- Morgan Magnin, Didier Lime, Olivier H. Roux:
An Efficient Method for Computing Exact State Space of Petri Nets With Stopwatches.
59-77
- Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani:
Model Checking Linear Programs with Arrays.
79-94
- Robert Palmer, Steve Barrus, Yu Yang, Ganesh Gopalakrishnan, Robert M. Kirby:
Gauss: A Framework for Verifying Scientific Computing Software.
95-106
- Steven P. Reiss:
Checking Event-Based Specifications in Java Systems.
107-132
- Bernd Westphal:
LSC Verification for UML Models with Unbounded Creation and Destruction.
133-145
Volume 144,
Number 4,
May 2006
Proceedings of the Fifth Workshop on Runtime Verification (RV 2005)
- Howard Barringer, Bernd Finkbeiner, Yuri Gurevich, Henny B. Sipma:
Preface.
1
- Feng Chen, Marcelo d'Amorim, Grigore Rosu:
Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP.
3-20
- Arvind Easwaran, Sampath Kannan, Oleg Sokolsky:
Steering of Discrete Event Systems: Control Theory Approach.
21-39
- Tayfun Elmas, Serdar Tasiran:
VyrdMC: Driving Runtime Refinement Checking with Model Checkers.
41-56
- Yaniv Eytani:
Concurrent Java Test Generation as a Search Problem.
57-72
- Amir Pnueli, Aleksandr Zaks, Lenore D. Zuck:
Monitoring Interfaces for Faults.
73-89
- Oleg Sokolsky, Usa Sammapun, Insup Lee, Jesung Kim:
Run-Time Checking of Dynamic Properties.
91-108
- Volker Stolz, Eric Bodden:
Temporal Assertions using AspectJ.
109-124
- Yuhong Zhao, Simon Oberthür, Martin Kardos, Franz-Josef Rammig:
Model-based Runtime Verification Framework for Self-optimizing Systems.
125-145
Copyright © Mon Mar 15 04:00:57 2010
by Michael Ley (ley@uni-trier.de)
