UPPAAL/DMC – Abstraction-Based Heuristics for Directed Model Checking (2009)
Sebastian Kupferschmid, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, Gerd Behrmann
Abstract. UPPAAL/DMC is an extension of UPPAAL which provides generic heuristics for directed model checking. In this approach, the traversal of the state space is guided by a heuristic function...
zur Erlangung des Grades (2009)
Andreas Rossberg, Dekan Prof, Dr. Thorsten Herfet, Vorsitzender Prfungsausschusses, ...
In this dissertation we develop an approach for reconciling open programming – the development of programs that support dynamic exchange of higher-order values with other processes – with strong...
Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, Heike Wehrheim
Abstract. Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In the paper [1], we present a new model checking procedure for...
der Universität des Saarlandes von (2008)
Andrey Rybalchenko, Dekan Prof, Dr. Jörg Eschmeier, Prüfungsausschuss Prof, Dr. Reinhard Wilhelm, ...
ii Program verification increases the degree of confidence that a program will perform correctly. Manual verification is an error-prone and tedious task. Its automation is highly desirable. The...
Bernd Finkbeiner, Henny B. Sipma
Abstract. We present an extension to linear-time temporal logic (LTL) that combines the temporal specification with the collection of statistical data. By collecting statistics over runtime...
Ø��Ý Ø�Ö� � ��ÐÐ�Ò��× � Ë�Ñ�ÒØ � �Ù�Ð�ØÝ � ÅË� × �ÜÔÖ�×× (2008)
×ÙÖ � Ø� � Ö�ÔÖ�×�ÒØ� � ÔÖÓÔ�ÖØÝ �Ò � � � � ÓÑÔÓ×� � �ÓÑ
Studies in Higher-Order Equational Logic (2008)
Prof Dr, Gert Smolka, Mark Kaminski, Verfasser Mark Kaminski, ...
Hiermit erkläre ich an Eides statt, dass ich die vorliegende Bachelorarbeit selbstständig verfasst und keine anderen als die angegebenen Quellen und Hilfsmittel verwendet habe. Saarbrücken, den 9....
07011 Executive Summary -- Runtime Verification (2008)
Finkbeiner, Bernd, Havelund, Klaus, Rosu, Grigore, Sokolsky, Oleg
From January 2 to January 6, 2007, the Dagstuhl Seminar 07011 ââ¬ËRuntime Verificationââ¬â¢ was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl....
07011 Abstracts Collection -- Runtime Verification (2008)
Finkbeiner, Bernd, Havelund, Klaus, Rosu, Grigore, Sokolsky, Oleg
From January 2--6 2007 the Dagstuhl Seminar 07011 {em `Runtime Verification'} was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several...
Abstraction Refinement for Games with Incomplete Information (2008)
Dimitrova, Rayna, Finkbeiner, Bernd
Counterexample-guided abstraction refinement (CEGAR) is used in automated software analysis to find suitable finite-state abstractions of infinite-state systems. In this paper, we extend CEGAR to...
RV'01 Preliminary Version Checking Finite Traces using Alternating Automata (2007)
We present three algorithms to check at runtime whether a reactive program satises a temporal specication, expressed by a future linear-time temporal logic formula. The three methods are all based on...
Nikolaj Bjrner, Anca Browne, Bernd Finkbeiner, Zohar Manna, Marc Pichora, Henny B. Sipma, ...
S Contents
Prof Dr, Bernd Finkbeiner, Dipl Inf, Klaus Dräger, Prof Dr, Bernd Finkbeiner, ...
This thesis presents an extension of deductive model checking that uses phase event automata to verify, if a given reactive system satisfies a specification, typically a temporal logic formula. Both...
Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, Heike Wehrheim
Abstract. Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for...
Eric Bodden, Mcgill Univeristy, Bernd Finkbeiner, Moonzoo Kim Kaist, Oege De Moor, Klaus Ostermann, ...
Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, Heike Wehrheim
Abstract. Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for...
Directed model checking with distance-preserving abstractions (2006)
Klaus Dräger, Bernd Finkbeiner, Andreas Podelski
Abstract. In directed model checking, the traversal of the state space is guided by an estimate of the distance from the current state to the nearest error state. This paper presents a...
Directed model checking with distance-preserving abstractions (2006)
Klaus Dräger, Bernd Finkbeiner, Andreas Podelski
Abstract. In directed model checking, the traversal of the state space is guided by an estimate of the distance from the current state to the nearest error state. This paper presents a...
Directed Model Checking with Distance-Preserving Abstractions (2006)
Dräge, Klaus, Finkbeiner, Bernd, Podelski, Andreas, Valmari, Antti
In directed model checking, the traversal of the state space is guided by an estimate of the distance from the current state to the nearest error state. This paper presents a distance-preserving...
A masters thesis advised by (2005)
Scott Cotton, Andreas Podelski, Bernd Finkbeiner
This thesis studies the problem of determining the satisfiability of a Boolean combination of binary difference constraints of the form x − y ≤ c where x and y are numeric variables and c is a...
Satisfiability checking with difference constraints (2005)
Scott Cotton, Andreas Podelski, Bernd Finkbeiner
This thesis studies the problem of determining the satisfiability of a Boolean combination of binary difference constraints of the form x − y ≤ c where x and y are numeric variables and c is a...
Verification algorithms based on alternating automata / (2002)
Finkbeiner, Bernd., Manna, Zohar Advisor
Submitted to the Department of Computer Science.
Collecting Statistics over Runtime Executions (2002)
Bernd Finkbeiner, Sriram Sankaranarayanan, Henny B. Sipma
Abstract. We present an extension to linear-time temporal logic (LTL) that combines the temporal specification with the collection of statistical data. By collecting statistics over runtime...
Language containment checking with nondeterministic BDDs (2001)
Abstract. Checking for language containment between nondeterministic!-automata is a central task in automata-based hierarchical verication. We present a symbolic procedure for language containment...
Checking Finite Traces using Alternating Automata (2001)
Abstract. Alternating automata have been commonly used as a basis for static verification of reactive systems. In this paper we show how alternating automata can be used in runtime verification. We...
Verifying temporal properties of reactive systems: A STeP tutorial (2000)
Nikolaj S. Bjørner, Anca Browne, Michael A. Colon, Bernd Finkbeiner, Zohar Manna, Henny B. Sipma, ...
We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery...
Abstraction and modular verification of infinite-state reactive systems (1998)
Zohar Manna, Michael A. Colon, Bernd Finkbeiner, Henny B. Sipma, Tomas E. Uribe
Abstract. We review a number of temporal verification techniques for reactive systems using modularity and abstraction. Their use allows the verification of larger systems, and the incremental...
Deductive verification of modular systems (1998)
Bernd Finkbeiner, Zohar Manna, Henny B. Sipma
Abstract. Effective verification methods, both deductive and algorithmic, exist for the verification of global system properties. In this paper, we introduce a formal framework for the modular...
Deductive verification of modular systems (1998)
Bernd Finkbeiner, Zohar Manna, Henny B. Sipma
Abstract. Effective verification methods, both deductive and algorithmic, exist for the verification of global system properties. In this paper, we introduce a formal framework for the modular...
Abstraction and Modular Verification of Infinite-State Reactive Systems (1998)
Zohar Manna, Michael A. Col'on, Bernd Finkbeiner, Henny B. Sipma, Tom'as E. Uribe
We review a number of temporal verification techniques for reactive systems using modularity and abstraction. Their use allows the verification of larger systems, and the incremental verification of...
STeP: The Stanford Temporal Prover Educational Release - User's Manual (1997)
Nikolaj Bjørner, Anca Browne, Eddie Chang, Michael Colón, Bernd Finkbeiner, Arjun Kapur, ...
This report complements the step manual by giving a high-level description of the system and its goals and some extra technical details. 3. The list of known problems and bugs known-bugs.txt.
STeP: Deductive-algorithmic verification of reactive and real-time systems (1996)
Zohar Manna, Nikolaj S. Bjrner, Anca Browne, Michael Colon, Bernd Finkbeiner, Mark Pichora, ...
Abstract. The Stanford Temporal Prover, STeP, is a tool for the computer-aided formal verification of reactive systems, including real-time and hybrid systems, based on their temporal specification....
STeP: Deductive-algorithmic verification of reactive and real-time systems (1996)
Zohar Manna, Nikolaj S. Bjrner, Anca Browne, Bernd Finkbeiner, Mark Pichora, Henny B. Sipma, ...
Abstract. The Stanford Temporal Prover, STeP, is a tool for the computer-aided formal verification of reactive systems, including real-time and hybrid systems, based on their temporal specification....
STeP: Deductive-algorithmic verification of reactive and real-time systems (1996)
Zohar Manna, Nikolaj S. Bjørner, Anca Browne, Michael Colón, Bernd Finkbeiner, Mark Pichora, ...
Abstract. The Stanford Temporal Prover, STeP, is a tool for the computer-aided formal verification of reactive systems, including real-time and hybrid systems, based on their temporal specification....
Principal faculty adviser: Daniel Chester, Dept. of Computer and Information Sciences.