8 Result(s)
-
Chapter
Regular Model Checking Revisited
In this contribution we revisit regular model checking, a powerful framework—pioneered by Bengt Jonsson et al.—that has been successfully applied for the verification of infinite-state systems, especially paramet...
-
Chapter and Conference Paper
Parameterized Synthesis with Safety Properties
Parameterized synthesis offers a solution to the problem of constructing correct and verified controllers for parameterized systems. Such systems occur naturally in practice (e.g., in the form of distributed p...
-
Chapter and Conference Paper
Monadic Decomposition in Integer Linear Arithmetic
Monadic decomposability is a notion of variable independence, which asks whether a given formula in a first-order theory is expressible as a Boolean combination of monadic predicates in the theory. Recently, V...
-
Chapter and Conference Paper
Probabilistic Bisimulation for Parameterized Systems
Probabilistic bisimulation is a fundamental not...
-
Chapter and Conference Paper
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
Word equations are a crucial element in the theoretical foundation of constraint solving over strings. A word equation relates two words over string variables and constants. Its solution amounts to a function ...
-
Chapter and Conference Paper
Complexity Analysis of Tree Share Structure
The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are hard to implement due to a la...
-
Chapter and Conference Paper
Fair Termination for Parameterized Probabilistic Concurrent Systems
We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameteri...
-
Chapter and Conference Paper
Regular Symmetry Patterns
Symmetry reduction is a well-known approach for alleviating the state explosion problem in model checking. Automatically identifying symmetries in concurrent systems, however, is computationally expensive. We ...
