1,721,117 research outputs found
Model Checking as Program Verification by Abstract Interpretation
No full textInterpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions based on (bi)simulation and property-preserving state relations have been successfully applied to abstract model checking. Here, we pursue a different track in which model checking is seen as an instance of program verification. To this purpose, we introduce a suitable language - called MOKA (for MOdel checking as abstract interpretation of Kleene Algebras) - which is used to encode temporal formulae as programs. In particular, we show that (universal fragments of) temporal logics, such as ACTL or, more generally, universal μ-calculus can be transformed into MOKA programs. Such programs return all and only the initial states which violate the formula. By applying abstract interpretation to MOKA programs, we pave the way for reusing more general abstractions than partitions as well as for tuning the precision of the abstraction to remove or avoid false alarms. We show how to perform model checking via a program logic that combines under-approximation and abstract interpretation analysis to avoid false alarms. The notion of locally complete abstraction is used to dynamically improve the analysis precision via counterexample-guided domain refinement
Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism
Full text linkWe present purity reflection, a programming language feature that enables higher-order functions to inspect the purity of their function arguments and to vary their behavior based on this information. The upshot is that operations on data structures can selectively use lazy and/or parallel evaluation while ensuring that side effects are never lost or re-ordered. The technique builds on a recent Hindley-Milner style type and effect system based on Boolean unification which supports both effect polymorphism and complete type inference. We illustrate that avoiding the so-called 'poisoning problem' is crucial to support purity reflection.
We propose several new data structures that use purity reflection to switch between eager and lazy, sequential and parallel evaluation. We propose a DelayList, which is maximally lazy but switches to eager evaluation for impure operations. We also propose a DelayMap which is maximally lazy in its values, but also exploits eager and parallel evaluation.
We implement purity reflection as an extension of the Flix programming language. We present a new effect-aware form of monomorphization that eliminates purity reflection at compile-time. And finally, we evaluate the cost of this new monomorphization on compilation time and on code size, and determine that it is minimal
Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits
Full text linkLayout synthesis is mapping a quantum circuit to a quantum processor. SWAP gate insertions are needed for scheduling 2-qubit gates only on connected physical qubits. With the ever-increasing number of qubits in NISQ processors, scalable layout synthesis is of utmost importance. With large optimality gaps observed in heuristic approaches, scalable exact methods are needed. While recent exact and near-optimal approaches scale to moderate circuits, large deep circuits are still out of scope. In this work, we propose a SAT encoding based on parallel plans that apply 1 SWAP and a group of CNOTs at each time step. Using domain-specific information, we maintain optimality in parallel plans while scaling to large and deep circuits. From our results, we show the scalability of our approach which significantly outperforms leading exact and near-optimal approaches (up to 100x). For the first time, we can optimally map several 8, 14, and 16 qubit circuits onto 54, 80, and 127 qubit platforms with up to 17 SWAPs. While adding optimal SWAPs, we also report near-optimal depth in our mapped circuits
Replication package with proofs for the paper "Operations on Fixpoint Equation Systems"
No full textThis archive contains mechanized proofs for the theorems and lemmas that appear in the paper Operations on Fixpoint Equation Systems, Thomas Neele and Jaco van de Pol This package contains proofs in both Coq and PVS. See the included README file for details on how to execute the proofs
Termination Proofs for Higher-order Rewrite Systems
No full textThis paper deals with termination proofs for Higher-Order Rewrite Systems (HRSs), introduced in [12]. This formalism combines the computational aspects of term rewriting and simply typed lambda calculus. The result is a proof technique for the termination of a HRS, similar to the proof technique "Termination by interpretation in a wellfounded monotone algebra", described in [8, 19]. The resulting technique is as follows: Choose a higher-order algebra with operations for each function symbol in the HRS, equipped with some well-founded partial ordering. The operations must be strictly monotonic in this ordering. This choice generates a model for the HRS. If the choice can be made in such a way that for each rule the interpretation of the left hand side is greater than the interpretation of the right hand side, then the HRS is terminating. At the end of the paper some applications of this technique are given, which show that this technique is natural and can easily be applied
Distributing requirements specifications on basic splice
Full text linkThis is an extension of work presented in [Jaco van de Pol-Expressiveness of Basic Splice. Report SEN-R0033, December 2000]. It is proved that the seemingly weak architecture Basic Splice introduced there --in which the coordination of processes is done using only a global set with read/write primitives-- can support a distributed implementation of a large class of requirements specifications, namely LPEs (a muCRL intermediate representation of specifications)
- …
