Showing 1–7 of 7 results for author: Nagele, J

Blockchain Superoptimizer

Authors: Julian Nagele, Maria A Schett

Abstract: In the blockchain-based, distributed computing platform Ethereum, programs called smart contracts are compiled to bytecode and executed on the Ethereum Virtual Machine (EVM). Executing EVM bytecode is subject to monetary fees---a clear optimization target. Our aim is to superoptimize EVM bytecode by encoding the operational semantics of EVM instructions as SMT formulas and leveraging a constraint… ▽ More In the blockchain-based, distributed computing platform Ethereum, programs called smart contracts are compiled to bytecode and executed on the Ethereum Virtual Machine (EVM). Executing EVM bytecode is subject to monetary fees---a clear optimization target. Our aim is to superoptimize EVM bytecode by encoding the operational semantics of EVM instructions as SMT formulas and leveraging a constraint solver to automatically find cheaper bytecode. We implement this approach in our EVM Bytecode SuperOptimizer ebso and perform two large scale evaluations on real-world data sets. △ Less

Submitted 12 May, 2020; originally announced May 2020.

Comments: 15 pages

Journal ref: Preproceedings of the 29th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2019), pp. 166-180, 2019

Confluence by Critical Pair Analysis Revisited (Extended Version)

Authors: Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi

Abstract: We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating. We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating. △ Less

Submitted 3 June, 2019; v1 submitted 28 May, 2019; originally announced May 2019.

Comments: Added a reference to the conference version

Critical Peaks Redefined - $Φ\sqcup Ψ= \top$

Authors: Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi

Abstract: Let a cluster be a term with a number of patterns occurring in it. We give two accounts of clusters, a geometric one as sets of (node and edge) positions, and an inductive one as pairs of terms with gaps (2nd order variables) and pattern-substitutions for the gaps. We show both notions of cluster and the corresponding refinement/coarsening orders on them, to be isomorphic. This equips clusters wit… ▽ More Let a cluster be a term with a number of patterns occurring in it. We give two accounts of clusters, a geometric one as sets of (node and edge) positions, and an inductive one as pairs of terms with gaps (2nd order variables) and pattern-substitutions for the gaps. We show both notions of cluster and the corresponding refinement/coarsening orders on them, to be isomorphic. This equips clusters with a lattice structure which we lift to (parallel/multi) steps to yield an alternative account of the notion of critical peak. △ Less

Submitted 25 August, 2017; originally announced August 2017.

Comments: 6th International Workshop on Confluence

Journal ref: In Proceedings of the 6th International Workshop on Confluence, pages 33 - 37, 2017

CoCoWeb - A Convenient Web Interface for Confluence Tools

Authors: Julian Nagele, Aart Middeldorp

Abstract: We present a useful web interface for tools that participate in the annual confluence competition. We present a useful web interface for tools that participate in the annual confluence competition. △ Less

Submitted 25 August, 2017; originally announced August 2017.

Comments: 6th International Workshop on Confluence

Journal ref: Proceedings of the 6th International Workshop on Confluence, pages 39 - 43, 2017

Certifying Confluence Proofs via Relative Termination and Rule Labeling

Authors: Julian Nagele, Bertram Felgenhauer, Harald Zankl

Abstract: The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certifi… ▽ More The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems. △ Less

Submitted 10 May, 2017; v1 submitted 21 December, 2016; originally announced December 2016.

ACM Class: F.2; F.4

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 2 (May 11, 2017) lmcs:3654

A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the $λβ$-calculus in Nominal Isabelle

Authors: Julian Nagele, Vincent van Oostrom, Christian Sternagel

Abstract: We present a short proof of the Church-Rosser property for the lambda-calculus enjoying two distinguishing features: Firstly, it employs the Z-property, resulting in a short and elegant proof; and secondly, it is formalized in the nominal higher-order logic available for the proof assistant Isabelle/HOL. We present a short proof of the Church-Rosser property for the lambda-calculus enjoying two distinguishing features: Firstly, it employs the Z-property, resulting in a short and elegant proof; and secondly, it is formalized in the nominal higher-order logic available for the proof assistant Isabelle/HOL. △ Less

Submitted 11 September, 2016; originally announced September 2016.

Comments: 5th International Workshop on Confluence

Journal ref: In Proceedings of the 5th International Workshop on Confluence, pages 55 - 59, 2016

Certification of Confluence Proofs using CeTA

Authors: Julian Nagele, René Thiemann

Abstract: CeTA was originally developed as a tool for certifying termination proofs which have to be provided as certificates in the CPF-format. Its soundness is proven as part of IsaFoR, the Isabelle Formalization of Rewriting. By now, CeTA can also be used for certifying confluence and non-confluence proofs. In this system description, we give a short overview on what kind of proofs are supported, and wha… ▽ More CeTA was originally developed as a tool for certifying termination proofs which have to be provided as certificates in the CPF-format. Its soundness is proven as part of IsaFoR, the Isabelle Formalization of Rewriting. By now, CeTA can also be used for certifying confluence and non-confluence proofs. In this system description, we give a short overview on what kind of proofs are supported, and what information has to be given in the certificates. As we will see, only a small amount of information is required and so we hope that CSI will not stay the only confluence tool which can produce certificates. △ Less

Submitted 6 May, 2015; originally announced May 2015.

Comments: 5 pages, International Workshop on Confluence 2014

Journal ref: In Proceedings of the 3rd International Workshop on Confluence, pages 19 - 23, 2014