Abstract The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of WPs is an important task with practical applications in areas ranging from verification to run-time error checking. This paper proposes the combination of Large Language Models (LLMs) and fuzz testing for generating WPs. In pursuit of this goal, we introduce Fuzzing Guidance (FG); FG acts as a means of directing LLMs towards correct WPs using program execution feedback. FG utilises fuzz testing for approximately checking the validity and weakness of candidate WPs, this information is then fed back to the LLM as a means of context refinement. We demonstrate the effectiveness of our approach on a comprehensive benchmark set of deterministic array programs in Java. Our experiments indicate that LLMs are capable of producing viable candidate WPs, and that this ability can be practically enhanced through FG.

We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF v ). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental bisimulation and game semantics. In order to obtain completeness while avoiding the use of semantic quotienting, the LTS constructs traces corresponding to interactions with possible functional contexts. The model gives rise to a sound and complete technique for checking of PCF v program equivalence, which we implement in a bounded bisimulation checking tool. We test our tool on known equivalences from the literature and new examples.

We propose Pushdown Normal Form (PDNF) Bisimulation to verify contextual equivalence in higher-order functional programming languages with local state. Similar to previous work on Normal Form (NF) bisimulation, PDNF Bisimulation is sound and complete with respect to contextual equivalence. However, unlike traditional NF Bisimulation, PDNF Bisimulation is also decidable for a class of program terms that can reach configurations of unbounded size, so long as the source of unboundedness is the call stack. Our approach relies on the principle that, in model-checking for reachability, pushdown systems can be simulated by finite-state automata designed to accept their initial/final stack content. We embody this in a stack-less Labelled Transition System (LTS), together with an on-the-fly saturation procedure for call stacks, upon which bisimulation is defined. We develop up-to techniques and a prototype implementation able to verify equivalences from the literature and others inspired by real code, which were out of reach for previous work.

We present the first fully abstract normal form bisimulation for call-by-value PCF (PCFv). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental bisimulation and game semantics. In order to obtain completeness while avoiding the use of semantic quotiening, the LTS constructs traces corresponding to interactions with possible functional contexts. The model gives rise to a sound and complete technique for checking of PCFvprogram equivalence, which we implement in a bounded bisimulation checking tool. We test our tool on known equivalences from the literature and new examples.

Abstract We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds. Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We realise the technique in a tool prototype called Hobbit and benchmark it with an extensive set of new and existing examples. Hobbit can prove many classical equivalences including all Meyer and Sieber examples.

We present a translation of CCS into CSP which is correct with respect to strong bisimulation. To our knowledge this is the first such translation to enjoy a correctness property. This contributes to the unification of the CCS and CSP families of concurrent calculi, in the spirit of Hoare and He’s unification programme through Unifying Theories of Programming. To facilitate this translation, we define CCSTau, the extension of CCS with visible synchronisation actions and the hiding operator. This separation of concerns between synchronisation and hiding turns out be sufficient to obtain our correct translation. Our translation, implemented in a Haskell prototype, makes it possible to use CSP-based verifiers such as FDR to reason about trace and failure (hence may- and must-testing) preorders for CCS processes.

We study the theory of safety and liveness in a reversible calculus where reductions are totally ordered and rollbacks lead systems to past states. Liveness and safety in this setting naturally correspond to the should-testing and inverse may-testing preorders, respectively. In reversible languages, however, the natural models of these preorders would need to be based on both forward and backward transitions, thus offering complex proof techniques for verification. Here we develop novel fully abstract models of liveness and safety which are based on forward transitions and limited rollback points, giving rise to considerably simpler proof techniques. Moreover, we show that, with respect to safety, total reversibility is a conservative extension to CCS. With respect to liveness, we prove that adding total reversibility to CCS distinguishes more systems. To our knowledge, this work provides the first testing theory for a reversible calculus, and paves the way for a testing theory for causal reversibility.

We introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including higher-order values, are storable. Our notion of bisimulation leads to smaller and more tractable relations than does the method of Sumii and Pierce [31]. In particular, our method allows one to write down a bisimulation relation directly in cases where [31] requires an inductive specification, and where the principle of local invariants [22] is inapplicable. Our method can also express examples with higher-order functions, in contrast with the most widely known previous methods [4, 22, 32] which are limited in their ability to deal with such examples. The bisimulation conditions are derived by manually extracting proof obligations from a hypothetical direct proof of contextual equivalence.