This paper presents the hrewrite library, that implements a term rewriting engine used as a backend for the generation of code assemblies. This library is implemented in C++ with a Python API, and accepts regular expression order-sorted term signatures and conditional rewriting rules. This paper describes the motivations of the library, its design, and illustrates it with some basic usage and with a discussion of its role as code assembly generation backend.
This paper presents an approach to checking the equivalence of quantum circuits based on Dirac notation in Maude. Specifically, we specify quantum states and quantum gates in Dirac notation with scalars and use a set of laws from quantum mechanics and matrix operations to reason about quantum computation. The equivalence of quantum circuits can be reduced to matrix equivalence modulo a global phase in Dirac notation. To achieve this, we compare each column vector of two matrices with respect to the same global phase, making it faster than the actual matrix equivalence check, especially in cases of non-equivalent quantum circuits. Furthermore, our approach enhances the reliability in determining the equivalence problem by taking into account constant inputs for quantum circuits, which have been ignored by state-of-the-art tools. We use Maude, a high-level specification/programming language based on rewriting logic, to develop a support tool called | QCEC⟩ for our approach. Several case studies have been conducted with the tool. These demonstrate the effectiveness of our approach and | QCEC⟩ for the equivalence checking of quantum circuits.
Verification of concurrent programs is very tough because the proof needs to account for a huge number of interleavings of execution steps of all threads. As concurrent programs are often implemented in C/C++, which do not support garbage collection, program verification needs to consider memory reclamation as well. In this paper, we report the safe memory verification of two concurrent programs integrated with hazard pointers, a mechanism for safe memory reclamation. We use CafeOBJ to formally specify the two programs and the properties of interest. The formal proofs are produced with the assistance of a tool called IPSG.
An equational theory ℰ=( , E ∪ B) is an equational program if its equations E, oriented as rewrite rules E⃗ , are ground convergent modulo axioms B. Its properties are the inductive theorems of the initial algebra 𝕋_ /E ∪ B defined by ( , E ∪ B) . Since programs are structured in module hierarchies, checkable syntactic conditions are given to preserve program properties up and/or down such hierarchies. Two equational programs ℰ=( , E ∪ B) and ℰ'=( , E' ∪ B') are equivalent iff they define the same computable functions on the same algebraic data types. Succinct conditions to verify ℰ and ℰ' equivalent are given. A useful internalization method to extend an equational program ℰ into an equivalent one by adding new rewrite rules or structural axioms that are inductive theorems of ℰ is also given. This method can make proofs of program properties simpler and shorter, and offers a new way to prove equational theories ground convergent.
We propose a new deductive model checking methodology where narrowing-based logical model checking of symbolic states specified as disjunctions of constrained patterns is synergistically combined with inductive theorem proving to discharge inductive verification conditions. An obvious synergy is to use an inductive theorem prover in automated mode as an oracle to help logical model checking reach a fixpoint. But this is not the only possible synergy. In this paper we focus instead on a new deductive model checking methodology to verify invariants-including inductive invariants-of infinite-state systems, where logical model checking automates large parts of the verification effort with the help of an inductive theorem prover as an oracle, and the remaining tasks are left to the inductive theorem prover used in interactive mode. We demonstrate this methodology by means of Maude examples using two tools working in tandem: the DM-Check symbolic model checker, and the NuITP inductive theorem prover.
