-
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny
Authors:
Franck Cassez,
Joanne Fuller,
Milad K. Ghale,
David J. Pearce,
Horacio M. A. Quiles
Abstract:
The Ethereum protocol implements a replicated state machine. The network participants keep track of the system state by: 1) agreeing on the sequence of transactions to be processed and 2) computing the state transitions that correspond to the sequence of transactions. Ethereum transactions are programs, called smart contracts, and computing a state transition requires executing some code. The Ethe…
▽ More
The Ethereum protocol implements a replicated state machine. The network participants keep track of the system state by: 1) agreeing on the sequence of transactions to be processed and 2) computing the state transitions that correspond to the sequence of transactions. Ethereum transactions are programs, called smart contracts, and computing a state transition requires executing some code. The Ethereum Virtual Machine (EVM) provides this capability and can execute programs written in EVM bytecode. We present a formal and executable semantics of the EVM written in the verification-friendly language Dafny: it provides (i) a readable, formal and verified specification of the semantics of the EVM; (ii) a framework to formally reason about bytecode.
△ Less
Submitted 28 February, 2023;
originally announced March 2023.
-
Finding Bugs with Specification-Based Testing is Easy!
Authors:
Janice Chin,
David Pearce
Abstract:
Automated specification-based testing has a long history with several notable tools having emerged. For example, QuickCheck for Haskell focuses on testing against user-provided properties. Others, such as JMLUnit, use specifications in the form of pre- and post-conditions to drive testing. An interesting (and under-explored) question is how effective this approach is at finding bugs in practice…
▽ More
Automated specification-based testing has a long history with several notable tools having emerged. For example, QuickCheck for Haskell focuses on testing against user-provided properties. Others, such as JMLUnit, use specifications in the form of pre- and post-conditions to drive testing. An interesting (and under-explored) question is how effective this approach is at finding bugs in practice. In general, one would assume automated testing is less effective at bug finding than static verification. But, how much less effective? To shed light on this question, we consider automated testing of programs written in Whiley -- a language with first-class support for specifications. Whilst originally designed with static verification in mind, we have anecdotally found automated testing for Whiley surprisingly useful and cost-effective. For example, when an error is detected with automated testing, a counterexample is always provided. This has motivated the more rigorous empirical examination presented in this paper. To that end, we provide a technical discussion of the implementation behind an automated testing tool for Whiley. Here, a key usability concern is the ability to parameterise the input space, and we present novel approaches for references and lambdas. We then report on several large experiments investigating the tool's effectiveness at bug finding using a range of benchmarks, including a suite of 1800+ mutants. The results indicate the automated testing is effective in many cases, and that sampling offers useful performance benefits with only modest reductions in bug-finding capability. Finally, we report on some real-world uses of the tool where it has proved effective at finding bugs (such as in the standard library).
△ Less
Submitted 26 February, 2021;
originally announced March 2021.
-
Putting the Semantics into Semantic Versioning
Authors:
Patrick Lam,
Jens Dietrich,
David J. Pearce
Abstract:
The long-standing aspiration for software reuse has made astonishing strides in the past few years. Many modern software development ecosystems now come with rich sets of publicly-available components contributed by the community. Downstream developers can leverage these upstream components, boosting their productivity.
However, components evolve at their own pace. This imposes obligations on an…
▽ More
The long-standing aspiration for software reuse has made astonishing strides in the past few years. Many modern software development ecosystems now come with rich sets of publicly-available components contributed by the community. Downstream developers can leverage these upstream components, boosting their productivity.
However, components evolve at their own pace. This imposes obligations on and yields benefits for downstream developers, especially since changes can be breaking, requiring additional downstream work to adapt to. Upgrading too late leaves downstream vulnerable to security issues and missing out on useful improvements; upgrading too early results in excess work. Semantic versioning has been proposed as an elegant mechanism to communicate levels of compatibility, enabling downstream developers to automate dependency upgrades.
While it is questionable whether a version number can adequately characterize version compatibility in general, we argue that developers would greatly benefit from tools such as semantic version calculators to help them upgrade safely. The time is now for the research community to develop such tools: large component ecosystems exist and are accessible, component interactions have become observable through automated builds, and recent advances in program analysis make the development of relevant tools feasible. In particular, contracts (both traditional and lightweight) are a promising input to semantic versioning calculators, which can suggest whether an upgrade is likely to be safe.
△ Less
Submitted 16 August, 2020;
originally announced August 2020.
-
Revisiting Explicit Negation in Answer Set Programming
Authors:
Felicidad Aguado,
Pedro Cabalar,
Jorge Fandinno,
David Pearce,
Gilberto Perez,
Concepcion Vidal
Abstract:
A common feature in Answer Set Programming is the use of a second negation, stronger than default negation and sometimes called explicit, strong or classical negation. This explicit negation is normally used in front of atoms, rather than allowing its use as a regular operator. In this paper we consider the arbitrary combination of explicit negation with nested expressions, as those defined by Lif…
▽ More
A common feature in Answer Set Programming is the use of a second negation, stronger than default negation and sometimes called explicit, strong or classical negation. This explicit negation is normally used in front of atoms, rather than allowing its use as a regular operator. In this paper we consider the arbitrary combination of explicit negation with nested expressions, as those defined by Lifschitz, Tang and Turner. We extend the concept of reduct for this new syntax and then prove that it can be captured by an extension of Equilibrium Logic with this second negation. We study some properties of this variant and compare to the already known combination of Equilibrium Logic with Nelson's strong negation. Under consideration for acceptance in TPLP.
△ Less
Submitted 26 July, 2019;
originally announced July 2019.
-
Functional ASP with Intensional Sets: Application to Gelfond-Zhang Aggregates
Authors:
Pedro Cabalar,
Jorge Fandinno,
Luis Fariñas del Cerro,
David Pearce
Abstract:
In this paper, we propose a variant of Answer Set Programming (ASP) with evaluable functions that extends their application to sets of objects, something that allows a fully logical treatment of aggregates. Formally, we start from the syntax of First Order Logic with equality and the semantics of Quantified Equilibrium Logic with evaluable functions (QELF). Then, we proceed to incorporate a new ki…
▽ More
In this paper, we propose a variant of Answer Set Programming (ASP) with evaluable functions that extends their application to sets of objects, something that allows a fully logical treatment of aggregates. Formally, we start from the syntax of First Order Logic with equality and the semantics of Quantified Equilibrium Logic with evaluable functions (QELF). Then, we proceed to incorporate a new kind of logical term, intensional set (a construct commonly used to denote the set of objects characterised by a given formula), and to extend QELF semantics for this new type of expression. In our extended approach, intensional sets can be arbitrarily used as predicate or function arguments or even nested inside other intensional sets, just as regular first-order logical terms. As a result, aggregates can be naturally formed by the application of some evaluable function (count, sum, maximum, etc) to a set of objects expressed as an intensional set. This approach has several advantages. First, while other semantics for aggregates depend on some syntactic transformation (either via a reduct or a formula translation), the QELF interpretation treats them as regular evaluable functions, providing a compositional semantics and avoiding any kind of syntactic restriction. Second, aggregates can be explicitly defined now within the logical language by the simple addition of formulas that fix their meaning in terms of multiple applications of some (commutative and associative) binary operation. For instance, we can use recursive rules to define sum in terms of integer addition. Last, but not least, we prove that the semantics we obtain for aggregates coincides with the one defined by Gelfond and Zhang for the Alog language, when we restrict to that syntactic fragment. (Under consideration for acceptance in TPLP)
△ Less
Submitted 2 May, 2018;
originally announced May 2018.
-
A Denotational Semantics for Equilibrium Logic
Authors:
Felicidad Aguado,
Pedro Cabalar,
David Pearce,
Gilberto Pérez,
Concepción Vidal
Abstract:
In this paper we provide an alternative semantics for Equilibrium Logic and its monotonic basis, the logic of Here-and-There (also known as Gödel's G3 logic) that relies on the idea of "denotation" of a formula, that is, a function that collects the set of models of that formula. Using the three-valued logic G3 as a starting point and an ordering relation (for which equilibrium/stable models are m…
▽ More
In this paper we provide an alternative semantics for Equilibrium Logic and its monotonic basis, the logic of Here-and-There (also known as Gödel's G3 logic) that relies on the idea of "denotation" of a formula, that is, a function that collects the set of models of that formula. Using the three-valued logic G3 as a starting point and an ordering relation (for which equilibrium/stable models are minimal elements) we provide several elementary operations for sets of interpretations. By analysing structural properties of the denotation of formulas, we show some expressiveness results for G3 such as, for instance, that conjunction is not expressible in terms of the other connectives. Moreover, the denotational semantics allows us to capture the set of equilibrium models of a formula with a simple and compact set expression. We also use this semantics to provide several formal definitions for entailment relations that are usual in the literature, and further introduce a new one called "strong entailment". We say that $α$ strongly entails $β$ when the equilibrium models of $α\wedge γ$ are also equilibrium models of $β\wedge γ$ for any context $γ$. We also provide a characterisation of strong entailment in terms of the denotational semantics, and give an example of a sufficient condition that can be applied in some cases.
△ Less
Submitted 24 July, 2015;
originally announced July 2015.
-
On the complexity of Temporal Equilibrium Logic
Authors:
Laura Bozzelli,
David Pearce
Abstract:
Temporal Equilibrium Logic (TEL) is a promising framework that extends the knowledge representation and reasoning capabilities of Answer Set Programming with temporal operators in the style of LTL. To our knowledge it is the first nonmonotonic logic that accommodates fully the syntax of a standard temporal logic (specifically LTL) without requiring further constructions. This paper provides a syst…
▽ More
Temporal Equilibrium Logic (TEL) is a promising framework that extends the knowledge representation and reasoning capabilities of Answer Set Programming with temporal operators in the style of LTL. To our knowledge it is the first nonmonotonic logic that accommodates fully the syntax of a standard temporal logic (specifically LTL) without requiring further constructions. This paper provides a systematic complexity analysis for the (consistency) problem of checking the existence of a temporal equilibrium model of a TEL formula. It was previously shown that this problem in the general case lies somewhere between PSPACE and EXPSPACE. Here we establish a lower bound matching the known EXPSPACE upper bound. Additionally we analyse the complexity for various natural subclasses of TEL formulas, identifying both tractable and intractable fragments. Finally the paper offers some new insights on the logic LTL by addressing satisfiability for minimal LTL models. The complexity results obtained highlight a substantial difference between interpreting LTL over finite or infinite words.
△ Less
Submitted 27 February, 2015;
originally announced March 2015.
-
Interpolable Formulas in Equilibrium Logic and Answer Set Programming
Authors:
Dov Gabbay,
David Pearce,
Agustín Valverde
Abstract:
Interpolation is an important property of classical and many non-classical logics that has been shown to have interesting applications in computer science and AI. Here we study the Interpolation Property for the the non-monotonic system of equilibrium logic, establishing weaker or stronger forms of interpolation depending on the precise interpretation of the inference relation. These results also…
▽ More
Interpolation is an important property of classical and many non-classical logics that has been shown to have interesting applications in computer science and AI. Here we study the Interpolation Property for the the non-monotonic system of equilibrium logic, establishing weaker or stronger forms of interpolation depending on the precise interpretation of the inference relation. These results also yield a form of interpolation for ground logic programs under the answer sets semantics. For disjunctive logic programs we also study the property of uniform interpolation that is closely related to the concept of variable forgetting. The first-order version of equilibrium logic has analogous Interpolation properties whenever the collection of equilibrium models is (first-order) definable. Since this is the case for so-called safe programs and theories, it applies to the usual situations that arise in practical answer set programming.
△ Less
Submitted 16 January, 2014;
originally announced January 2014.
-
Interpolation in Equilibrium Logic and Answer Set Programming: the Propositional Case
Authors:
Dov Gabbay,
David Pearce,
Agustí n Valverde
Abstract:
Interpolation is an important property of classical and many non classical logics that has been shown to have interesting applications in computer science and AI. Here we study the Interpolation Property for the propositional version of the non-monotonic system of equilibrium logic, establishing weaker or stronger forms of interpolation depending on the precise interpretation of the inference rela…
▽ More
Interpolation is an important property of classical and many non classical logics that has been shown to have interesting applications in computer science and AI. Here we study the Interpolation Property for the propositional version of the non-monotonic system of equilibrium logic, establishing weaker or stronger forms of interpolation depending on the precise interpretation of the inference relation. These results also yield a form of interpolation for ground logic programs under the answer sets semantics. For disjunctive logic programs we also study the property of uniform interpolation that is closely related to the concept of variable forgetting.
△ Less
Submitted 17 December, 2010;
originally announced December 2010.
-
Characterising equilibrium logic and nested logic programs: Reductions and complexity
Authors:
David Pearce,
Hans Tompits,
Stefan Woltran
Abstract:
Equilibrium logic is an approach to nonmonotonic reasoning that extends the stable-model and answer-set semantics for logic programs. In particular, it includes the general case of nested logic programs, where arbitrary Boolean combinations are permitted in heads and bodies of rules, as special kinds of theories. In this paper, we present polynomial reductions of the main reasoning tasks associa…
▽ More
Equilibrium logic is an approach to nonmonotonic reasoning that extends the stable-model and answer-set semantics for logic programs. In particular, it includes the general case of nested logic programs, where arbitrary Boolean combinations are permitted in heads and bodies of rules, as special kinds of theories. In this paper, we present polynomial reductions of the main reasoning tasks associated with equilibrium logic and nested logic programs into quantified propositional logic, an extension of classical propositional logic where quantifications over atomic formulas are permitted. We provide reductions not only for decision problems, but also for the central semantical concepts of equilibrium logic and nested logic programs. In particular, our encodings map a given decision problem into some formula such that the latter is valid precisely in case the former holds. The basic tasks we deal with here are the consistency problem, brave reasoning, and skeptical reasoning. Additionally, we also provide encodings for testing equivalence of theories or programs under different notions of equivalence, viz. ordinary, strong, and uniform equivalence. For all considered reasoning tasks, we analyse their computational complexity and give strict complexity bounds.
△ Less
Submitted 13 June, 2009; v1 submitted 11 June, 2009;
originally announced June 2009.
-
A Polynomial Translation of Logic Programs with Nested Expressions into Disjunctive Logic Programs: Preliminary Report
Authors:
David Pearce,
Vladimir Sarsakov,
Torsten Schaub,
Hans Tompits,
Stefan Woltran
Abstract:
Nested logic programs have recently been introduced in order to allow for arbitrarily nested formulas in the heads and the bodies of logic program rules under the answer sets semantics. Nested expressions can be formed using conjunction, disjunction, as well as the negation as failure operator in an unrestricted fashion. This provides a very flexible and compact framework for knowledge represent…
▽ More
Nested logic programs have recently been introduced in order to allow for arbitrarily nested formulas in the heads and the bodies of logic program rules under the answer sets semantics. Nested expressions can be formed using conjunction, disjunction, as well as the negation as failure operator in an unrestricted fashion. This provides a very flexible and compact framework for knowledge representation and reasoning. Previous results show that nested logic programs can be transformed into standard (unnested) disjunctive logic programs in an elementary way, applying the negation as failure operator to body literals only. This is of great practical relevance since it allows us to evaluate nested logic programs by means of off-the-shelf disjunctive logic programming systems, like DLV. However, it turns out that this straightforward transformation results in an exponential blow-up in the worst-case, despite the fact that complexity results indicate that there is a polynomial translation among both formalisms. In this paper, we take up this challenge and provide a polynomial translation of logic programs with nested expressions into disjunctive logic programs. Moreover, we show that this translation is modular and (strongly) faithful. We have implemented both the straightforward as well as our advanced transformation; the resulting compiler serves as a front-end to DLV and is publicly available on the Web.
△ Less
Submitted 19 July, 2002;
originally announced July 2002.
