critic
发表于 2025-3-23 11:15:15
An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutab has blossomed recently, with many different approaches all showing leaps in performance and expressiveness. A year ago, we proposed a small logic for specifying predicates about HMPs and demonstrated that an inference-rule-based decision procedure could be performance-competitive, and in many cases
龙卷风
发表于 2025-3-23 14:26:29
On Flat Programs with Listsly-linked list data structures. Since, in general, programs with lists are known to have the power of Turing machines, we restrict the control structure, by forbidding nested loops and destructive updates. Surprisingly, even with these simplifying conditions, verifying safety and termination for pro
涂掉
发表于 2025-3-23 21:01:36
Automata-Theoretic Model Checking RevisitedWe then use graph algorithms to search for a counterexample trace. The basic theory of this approach was worked out in the 1980s, and the basic algorithms were developed during the 1990s. Both explicit and symbolic implementations, such as SPIN and and SMV, are widely used. It turns out, however, th
CAJ
发表于 2025-3-23 23:53:40
http://reply.papertrans.cn/99/9818/981728/981728_14.png
无意
发表于 2025-3-24 05:01:06
More Precise Partition Abstractionsition set as state space. These variants are defined via satisfaction parity games in which the Refuter can replace a concrete state with any state in the same partition before, respectively after, a quantifier move. These games are independent of the kind of abstraction. Our first variant makes the
Frisky
发表于 2025-3-24 07:10:25
The Spotlight Principleomain local data is challenging due to the two sources of infiniteness. The existing state abstraction-based approaches Data Type Reduction and Environment Abstraction each address one aspect, but the former doesn’t support infinite-domain local data and the latter doesn’t support links and is restr
助记
发表于 2025-3-24 12:12:00
Lattice Automatant, rather than a Boolean value. The automata-theoretic approach for reasoning about Boolean-valued systems has proven to be very useful and powerful. We develop an automata-theoretic framework for reasoning about multi-valued objects, and describe its application. The basis to our framework are . o
灌输
发表于 2025-3-24 15:24:55
Learning Algorithms and Formal Verification (Invited Tutorial)els for learning formally representable concepts using either positive and negative samples or by access to an oracle that can answer certain queries about the concept..The problem of learning formal languages has been particularly useful in verification applications. We will introduce Angluin’s alg
Benign
发表于 2025-3-24 21:04:18
http://reply.papertrans.cn/99/9818/981728/981728_19.png
exorbitant
发表于 2025-3-25 02:17:50
Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning as doubly-linked lists. The algorithm abstracts and analyzes one single heap cell at a time. In order to maintain the structural invariants, the analysis uses a local heap abstraction that models the sub-heap consisting of one cell and its immediate neighbors. The proposed algorithm can successfull