![Loading...](https://link.springer.com/static/c4a417b97a76cc2980e3c25e2271af3129e08bbe/images/pdf-preview/spacer.gif)
-
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
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
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 ...