26 Result(s)

Chapter and Conference Paper

A Python Library for Trace Analysis

We present a Python library for trace analysis named PyContract. PyContract is a shallow internal DSL, in contrast to many trace analysis tools that implement external or deep internal DSLs. The library has be...

Dennis Dams, Klaus Havelund, Sean Kauffman in Runtime Verification (2022)

Chapter and Conference Paper

Runtime Verification as Documentation

In runtime verification, a monitor is used to return a Boolean verdict on the behavior of a system. We present several examples of the use of monitors to instead document system behavior. In doing so, we demonstr...

Dennis Dams, Klaus Havelund, Sean Kauffman in Leveraging Applications of Formal Methods,… (2022)

Chapter

Abstraction and Abstraction Refinement

Abstraction, in the context of model checking, is aimed at reducing the state space of the system by omitting details that are irrelevant to the property being verified. Many successful approaches to the “stat...

Dennis Dams, Orna Grumberg in Handbook of Model Checking (2018)

Chapter

A Bibliography of Willem-Paul de Roever

Dennis Dams, Ulrich Hannemann… in Concurrency, Compositionality, and Correct… (2010)

Chapter and Conference Paper

Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors

It is well known that the use of points-to information can substantially improve the accuracy of a static program analysis. Commonly used algorithms for computing points-to information are known to be sound on...

Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, Clark Barrett in Static Analysis (2008)

Chapter and Conference Paper

StackSnuffer: Curing Orion’s Unsoundness

Software analysis and verification require abstraction of the program under consideration. As a result, many reported errors may in fact be false alarms. The Orion static analyzer reduces the ratio of false al...

Dennis Dams in Model Checking Software (2007)

Chapter and Conference Paper

Automata as Abstractions

We propose the use of tree automata as abstractions in the verification of branching time properties, and show several benefits. In this setting, soundness and completeness are trivial. It unifies the abundanc...

Dennis Dams, Kedar S. Namjoshi in Verification, Model Checking, and Abstract Interpretation (2005)

Chapter and Conference Paper

Shape Analysis through Predicate Abstraction and Model Checking

We propose a new framework, based on predicate abstraction and model checking, for shape analysis of programs. Shape analysis is used to statically collect information—such as possible reachability and sharing—ab...

Dennis Dams, Kedar S. Namjoshi in Verification, Model Checking, and Abstract Interpretation (2003)

Article

Symmetric Spin

We give a detailed description of SymmSpin, a prototype implementation of a symmetry-reduction package for the Spin model checker. It offers several heuristics for state-space reduction. A series of experiment...

Dragan Bošnački, Dennis Dams… in International Journal on Software Tools fo… (2002)

Chapter and Conference Paper

Abstraction in Software Model Checking: Principles and Practice

This paper provides a brief description, including a bibliography, of the SPIN2002 tutorial on abstraction in model checking of software.

Dennis Dams in Model Checking Software (2002)

Chapter and Conference Paper

A Heuristic for Symmetry Reductions with Scalarsets

We present four versions of a new heuristic for co** with the problem of finding (canonical) representatives of symmetry equivalence classes (the so-called orbit problem), in symmetry techniques for model check...

Dragan Bošnački, Leszek Holenderski… in FME 2001: Formal Methods for Increasing So… (2001)

Chapter and Conference Paper

An On-the-Fly Tableau Construction for a Real-Time Temporal Logic

Temporal logic is a useful tool for specifying correctness properties of reactive programs. In particular, real-time temporal logics have been developed for expressing quantitative timing aspects of systems. A...

Marc Geilen, Dennis Dams in Formal Techniques in Real-Time and Fault-Tolerant Systems (2000)

Chapter and Conference Paper

Symmetric Spin

We give a detailed description of SymmSpin, a symmetry-reduction package for Spin. It offers four strategies for state-space reduction, based on the heuristic that we presented in [3], and a fifth mode for ref...

Dragan Bošnački, Dennis Dams… in SPIN Model Checking and Software Verificat… (2000)