Journal: Electronic Notes in Theoretical Computer Science

Volume 144, Issue 4

1 -- 0Howard Barringer, Bernd Finkbeiner, Yuri Gurevich, Henny B. Sipma. Preface
3 -- 20Feng Chen, Marcelo d Amorim, Grigore Rosu. Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP
21 -- 39Arvind Easwaran, Sampath Kannan, Oleg Sokolsky. Steering of Discrete Event Systems: Control Theory Approach
41 -- 56Tayfun Elmas, Serdar Tasiran. VyrdMC: Driving Runtime Refinement Checking with Model Checkers
57 -- 72Yaniv Eytani. Concurrent Java Test Generation as a Search Problem
73 -- 89Amir Pnueli, Aleksandr Zaks, Lenore D. Zuck. Monitoring Interfaces for Faults
91 -- 108Oleg Sokolsky, Usa Sammapun, Insup Lee, Jesung Kim. Run-Time Checking of Dynamic Properties
109 -- 124Volker Stolz, Eric Bodden. Temporal Assertions using AspectJ
125 -- 145Yuhong Zhao, Simon Oberthür, Martin Kardos, Franz-Josef Rammig. Model-based Runtime Verification Framework for Self-optimizing Systems

Volume 144, Issue 3

1 -- 2Byron Cook, Scott D. Stoller, Willem Visser. Preface
3 -- 26Wolfgang Grieskamp, Nikolai Tillmann, Wolfram Schulte. XRT- Exploring Runtime for .NET Architecture and Applications
27 -- 44Radu Grosu, Xiaowan Huang, Sumit Jain, Scott A. Smolka. Open-Source Model Checking
45 -- 58Graham Hughes, Sreeranga P. Rajan, Tom Sidle, Keith Swenson. Error Detection in Concurrent Java Programs
59 -- 77Morgan Magnin, Didier Lime, Olivier H. Roux. An Efficient Method for Computing Exact State Space of Petri Nets With Stopwatches
79 -- 94Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani. Model Checking Linear Programs with Arrays
95 -- 106Robert Palmer, Steve Barrus, Yu Yang, Ganesh Gopalakrishnan, Robert M. Kirby. Gauss: A Framework for Verifying Scientific Computing Software
107 -- 132Steven P. Reiss. Checking Event-Based Specifications in Java Systems
133 -- 145Bernd Westphal. LSC Verification for UML Models with Unbounded Creation and Destruction

Volume 144, Issue 2

1 -- 2Alessandro Armando, Alessandro Cimatti. Preface
3 -- 14Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani. Encoding RTL Constructs for MathSAT: a Preliminary Report
15 -- 26Jim Grundy, Thomas F. Melham, Sava Krstic, Sean McLaughlin. Tool Building Requirements for an API to First-Order Solvers
27 -- 41Shuvendu K. Lahiri, Madanlal Musuvathi. An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
43 -- 51Sean McLaughlin, Clark Barrett, Yeting Ge. Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite
53 -- 65Amir Pnueli, Ofer Strichman. Reduced Functional Consistency of Uninterpreted Functions
67 -- 78Tjark Weber. Integrating a SAT Solver with an LCF-style Theorem Prover
79 -- 91Ian Wehrman, Aaron Stump. Mining Propositional Simplification Proofs for Small Validating Clauses

Volume 144, Issue 1

1 -- 0Armin Biere, Ofer Strichman. Preface
3 -- 18Markus Jehle, Jan Johannsen, Martin Lange, Nicolas Rachinsky. Bounded Model Checking for All Regular Properties
19 -- 33Anders Franzén. Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs
35 -- 50Ohad Shacham, Karen Yorav. Adaptive Application of SAT Solving Techniques
51 -- 66Mohammad Awedh, Fabio Somenzi. Termination Criteria for Bounded Model Checking: Extensions and Comparison
67 -- 77Daniel Geist, Mark Ginzburg, Yoad Lustig, Ishai Rabinovitz, Ohad Shacham, Rachel Tzoref. Supporting SAT based BMC on Finite Path Models
79 -- 92Daniel Kroening. Computing Over-Approximations with Bounded Model Checking