1,553 papers · page 28 of 78
Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with \omega-regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the…
Abstract elided by the publisher.
Abstract elided by the publisher.
This paper contributes to the trend of providing fully verified container libraries. We consider an implementation of the bounded doubly linked list container which manages the list in a fixed size, heap allocated array. The container provides constant time methods to update the …
Abstract elided by the publisher.
Abstract elided by the publisher.
We propose a method for automatically finding refinement types of higher-order function programs. Our method is an extension of the Ice framework of Garg et al. for finding invariants. In addition to the usual positive and negative samples in machine learning, their Ice framework…
Abstract elided by the publisher.
Specification decomposition is a theoretically interesting and practically relevant problem for which two approaches were independently developed by the control theory and verification communities: natural projection and partial model checking. In this paper we show that, under r…
Abstract elided by the publisher.
Abstract elided by the publisher.
Ultimate Taipan is a software model checker that uses trace abstraction and abstract interpretation to prove correctness of programs. In contrast to previous versions, Ultimate Taipan now uses dynamic block encoding to obtain the best precision possible when evaluating transition…
Parity games have important practical applications in formal verification and synthesis, especially to solve the model-checking problem of the modal mu-calculus. They are also interesting from the theory perspective, as they are widely believed to admit a polynomial solution, but…
Abstract elided by the publisher.
Abstract elided by the publisher.
Modern system design often requires comparing several models over a large design space. Different models arise out of a need to weigh different design choices, to check core capabilities of versions with varying features, or to analyze a future version against previous ones. Mode…
We present a fast algorithm for syntax-guided synthesis of inductive invariants which combines enumerative learning with inductive-subset extraction, leverages counterexamples-to-induction and interpolation-based bounded proofs. It is a variant of a recently proposed probabilisti…
We present \(\text {RVHyper}\), a runtime verification tool for hyperproperties. Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. Specifications are given as formulas in the temporal logic \(\text {HyperL…
Abstract elided by the publisher.
We study three different Hoare logics for reasoning about time bounds of imperative programs and formalize them in Isabelle/HOL: a classical Hoare like logic due to Nielson, a logic with potentials due to Carbonneaux et al. and a separation logic following work by Atkey, Chaguera…