Workshop CPP 2019 – Author Index 
Contents 
Abstracts 
Authors

B C D E F G H I K L M P R S T V W X Y Z
Benzaken, Véronique 
CPP '19: "A Coq Mechanised Formal Semantics ..."
A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra
Véronique Benzaken and Évelyne Contejean (University of ParisSud, France; LRI, France; CNRS, France) In this article, we provide a Coq mechanised, executable, formal semantics for a realistic fragment of SQL consisting of "select [distinct] from where group by having" queries with null values, functions, aggregates, quantifiers and nested potentially correlated subqueries. Relying on the Coq extraction mechanism to Ocaml, we further produce a Coq certified semantic analyser for a SQL compiler. We then relate this fragment to a Coq formalised (extended) relational algebra that enjoys a bag semantics hence recovering all wellknown algebraic equivalences upon which are based most of compilation optimisations. By doing so, we provide the first formally mechanised proof of the equivalence of SQL and extended relational algebra. @InProceedings{CPP19p249, author = {Véronique Benzaken and Évelyne Contejean}, title = {A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {249261}, doi = {10.1145/3293880.3294107}, year = {2019}, } Publisher's Version Article Search 

Beringer, Lennart 
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Liyao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA) We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by lowlevel buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. @InProceedings{CPP19p234, author = {Nicolas Koh and Yao Li and Yishuai Li and Liyao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {234248}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version Article Search 

Blanchette, Jasmin Christian 
CPP '19: "A Verified Prover Based on ..."
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel (DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland) The superposition calculus, which underlies firstorder theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional firstorder ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for firstorder logic. @InProceedings{CPP19p152, author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel}, title = {A Verified Prover Based on Ordered Resolution}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {152165}, doi = {10.1145/3293880.3294100}, year = {2019}, } Publisher's Version Article Search CPP '19: "Formalizing the Metatheory ..." Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk) Jasmin Christian Blanchette (Vrije Universiteit Amsterdam, Netherlands) IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: a firstorder resolution prover, an imperative SAT solver, and generalized term orders for λfree higherorder logic. @InProceedings{CPP19p1, author = {Jasmin Christian Blanchette}, title = {Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {113}, doi = {10.1145/3293880.3294087}, year = {2019}, } Publisher's Version Article Search 

Blazy, Sandrine 
CPP '19: "Formal Verification of a Program ..."
Formal Verification of a Program Obfuscation Based on Mixed BooleanArithmetic Expressions
Sandrine Blazy and Rémi Hutin (University of Rennes, France; Inria, France; CNRS, France; IRISA, France) The insertion of expressions mixing arithmetic operators and bitwise boolean operators is a widespread protection of sensitive data in source programs. This recent advanced obfuscation technique is one of the less studied among program obfuscations even if it is commonly found in binary code. In this paper, we formally verify in Coq this data obfuscation. It operates over a generic notion of mixed booleanarithmetic expressions and on properties of bitwise operators operating over machine integers. Our obfuscation performs two kinds of program transformations: rewriting of expressions and insertion of modular inverses. To facilitate its proof of correctness, we define boolean semantic tables, a data structure inspired from truth tables. Our obfuscation is integrated into the CompCert formally verified compiler where it operates over Clight programs. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results. @InProceedings{CPP19p196, author = {Sandrine Blazy and Rémi Hutin}, title = {Formal Verification of a Program Obfuscation Based on Mixed BooleanArithmetic Expressions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {196208}, doi = {10.1145/3293880.3294103}, year = {2019}, } Publisher's Version Article Search Info 

Chaudhuri, Kaustuv 
CPP '19: "A ProofTheoretic Approach ..."
A ProofTheoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller (Inria, France; LIX, France; École Polytechnique, France) When presented with a formula to prove, most theorem provers for classical firstorder logic process that formula following several steps, one of which is commonly called skolemization. That process eliminates quantifier alternation within formulas by extending the language of the underlying logic with new Skolem functions and by instantiating certain quantifiers with terms built using Skolem functions. In this paper, we address the problem of checking (i.e., certifying) proof evidence that involves Skolem terms. Our goal is to do such certification without using the mathematical concepts of modeltheoretic semantics (i.e., preservation of satisfiability) and choice principles (i.e., epsilon terms). Instead, our proof checking kernel is an implementation of Gentzen's sequent calculus, which directly supports quantifier alternation by using eigenvariables. We shall describe deskolemization as a mapping from clientside terms, used in proofs generated by theorem provers, into kernelside terms, used within our proof checking kernel. This mapping which associates skolemized terms to eigenvariables relies on using outer skolemization. We also point out that the removal of Skolem terms from a proof is influenced by the polarities given to propositional connectives. @InProceedings{CPP19p78, author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller}, title = {A ProofTheoretic Approach to Certifying Skolemization}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {7890}, doi = {10.1145/3293880.3294094}, year = {2019}, } Publisher's Version Article Search 

Contejean, Évelyne 
CPP '19: "A Coq Mechanised Formal Semantics ..."
A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra
Véronique Benzaken and Évelyne Contejean (University of ParisSud, France; LRI, France; CNRS, France) In this article, we provide a Coq mechanised, executable, formal semantics for a realistic fragment of SQL consisting of "select [distinct] from where group by having" queries with null values, functions, aggregates, quantifiers and nested potentially correlated subqueries. Relying on the Coq extraction mechanism to Ocaml, we further produce a Coq certified semantic analyser for a SQL compiler. We then relate this fragment to a Coq formalised (extended) relational algebra that enjoys a bag semantics hence recovering all wellknown algebraic equivalences upon which are based most of compilation optimisations. By doing so, we provide the first formally mechanised proof of the equivalence of SQL and extended relational algebra. @InProceedings{CPP19p249, author = {Véronique Benzaken and Évelyne Contejean}, title = {A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {249261}, doi = {10.1145/3293880.3294107}, year = {2019}, } Publisher's Version Article Search 

Delaware, Benjamin 
CPP '19: "A Verified Protocol Buffer ..."
A Verified Protocol Buffer Compiler
Qianchuan Ye and Benjamin Delaware (Purdue University, USA) The code responsible for serializing and deserializing untrusted external data is a vital component of any software that communicates with the outside world, as any bugs in these components can compromise the entire system. This is particularly true for verified systems which rely on trusted code to process external data, as any defects in the parsing code can invalidate any formal proofs about the system. One way to reduce the trusted code base of these systems is to use interface generators like Protocol Buffer and ASN.1 to generate serializers and deserializers from data descriptors. Of course, these generators are not immune to bugs. In this work, we formally verify a compiler for a realistic subset of the popular Protocol Buffer serialization format using the Coq proof assistant, proving once and for all the correctness of every generated serializer and deserializer. One of the challenges we had to overcome was the extreme flexibility of the Protocol Buffer format: the same source data can be encoded in an infinite number of ways, and the deserializer must faithfully recover the original source value from each. We have validated our verified system using the official conformance tests. @InProceedings{CPP19p222, author = {Qianchuan Ye and Benjamin Delaware}, title = {A Verified Protocol Buffer Compiler}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {222233}, doi = {10.1145/3293880.3294105}, year = {2019}, } Publisher's Version Article Search Artifacts Available 

Eberl, Manuel 
CPP '19: "Verified Solving and Asymptotics ..."
Verified Solving and Asymptotics of Linear Recurrences
Manuel Eberl (TU Munich, Germany) Linear recurrences with constant coefficients are an interesting class of recurrence equations that can be solved explicitly. The most famous example are certainly the Fibonacci numbers with the equation f(n) = f(n−1) + f(n−2) and the quite nonobvious closed form 1√5 (ϕ^{n} − (−ϕ)^{−n}) where ϕ is the golden ratio. This work builds on existing tools in Isabelle – such as formal power series and polynomial factorisation algorithms – to develop a theory of these recurrences and derive a fully executable solver for them that can be exported to programming languages like Haskell. Based on this development, I also provide an efficient method to prove ‘BigO’ asymptotics of a solution automatically without explicitly finding the closedform solution first. @InProceedings{CPP19p27, author = {Manuel Eberl}, title = {Verified Solving and Asymptotics of Linear Recurrences}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {2737}, doi = {10.1145/3293880.3294090}, year = {2019}, } Publisher's Version Article Search Info 

Felgenhauer, Bertram 
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear VariableSeparated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp (University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria) It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variableseparated rewrite systems. To this end, we formalize procedures for ground tree transducers and socalled RR_{n} relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the firstorder theory of ground rewriting for linear, variableseparated rewrite systems. It forms the basis for a formalized confluence checker for leftlinear, rightground systems. @InProceedings{CPP19p132, author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp}, title = {A Verified Ground Confluence Tool for Linear VariableSeparated Rewrite Systems in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {132143}, doi = {10.1145/3293880.3294098}, year = {2019}, } Publisher's Version Article Search 

Felty, Amy P. 
CPP '19: "A Linear Logical Framework ..."
A Linear Logical Framework in Hybrid (Invited Talk)
Amy P. Felty (University of Ottawa, Canada) We present a linear logical framework implemented within the Hybrid system [Felty and Momigliano 2012]. Hybrid is designed to support the use of higherorder abstract syntax for representing and reasoning about formal systems, implemented in the Coq Proof Assistant. In this work, we extend the system with a linear specification logic, which provides infrastructure for reasoning directly about object languages with linear features. We developed this framework in order to address the challenges of reasoning about the type system of a quantum lambda calculus. In particular, we started by considering the ProtoQuipper language [Ross 2015], which contains the core of Quipper [Green et al. 2013; Selinger and Val iron 2006]. Quipper is a new quantum programming language under active development with a linear type system. We have completed a formal proof of type soundness for ProtoQuipper [Mahmoud and Felty 2018b]. Our current work includes extending this work to other properties of ProtoQuipper as well as reasoning about other quantum programming languages [Mahmoud and Felty 2018a]. It also includes reasoning about other object languages with linear features in areas such as metatheory of lowlevel abstract machine code, proof theory of focused linear sequent calculi, and modeling biological processes as transition systems and proving properties about them [Despeyroux et al. 2018]. @InProceedings{CPP19p14, author = {Amy P. Felty}, title = {A Linear Logical Framework in Hybrid (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1414}, doi = {10.1145/3293880.3294088}, year = {2019}, } Publisher's Version Article Search 

Forster, Yannick 
CPP '19: "CallByPushValue in Coq: ..."
CallByPushValue in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark (Saarland University, Germany) Callbypushvalue (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both callbyvalue (CBV) and callbyname (CBN). We formalise weak and strong operational semantics for (effectfree) CBPV, define its equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full λcalculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs. @InProceedings{CPP19p118, author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark}, title = {CallByPushValue in Coq: Operational, Equational, and Denotational Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {118131}, doi = {10.1145/3293880.3294097}, year = {2019}, } Publisher's Version Article Search Info CPP '19: "On Synthetic Undecidability ..." On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem Yannick Forster, Dominik Kirst, and Gert Smolka (Saarland University, Germany) We formalise the computational undecidability of validity, satisfiability, and provability of firstorder formulas following a synthetic approach based on the computation native to Coq's constructive type theory. Concretely, we consider Tarski and Kripke semantics as well as classical and intuitionistic natural deduction systems and provide compact manyone reductions from the Post correspondence problem (PCP). Moreover, developing a basic framework for synthetic computability theory in Coq, we formalise standard results concerning decidability, enumerability, and reducibility without reference to a concrete model of computation. For instance, we prove the equivalence of Post's theorem with Markov's principle and provide a convenient technique for establishing the enumerability of inductive predicates such as the considered proof systems and PCP. @InProceedings{CPP19p38, author = {Yannick Forster and Dominik Kirst and Gert Smolka}, title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3851}, doi = {10.1145/3293880.3294091}, year = {2019}, } Publisher's Version Article Search Info CPP '19: "Certified Undecidability of ..." Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines Yannick Forster and Dominique LarcheyWendling (Saarland University, Germany; University of Lorraine, France; CNRS, France; LORIA, France) We formally prove the undecidability of entailment in intuitionistic linear logic in Coq. We reduce the Post correspondence problem (PCP) via binary stack machines and Minsky machines to intuitionistic linear logic. The reductions rely on several technically involved formalisations, amongst them a binary stack machine simulator for PCP, a verified lowlevel compiler for instructionbased languages and a soundness proof for intuitionistic linear logic with respect to trivial phase semantics. We exploit the computability of all functions definable in constructive type theory and thus do not have to rely on a concrete model of computation, enabling the reduction proofs to focus on correctness properties. @InProceedings{CPP19p104, author = {Yannick Forster and Dominique LarcheyWendling}, title = {Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {104117}, doi = {10.1145/3293880.3294096}, year = {2019}, } Publisher's Version Article Search Info 

Gunter, Elsa L. 
CPP '19: "Dynamic Class Initialization ..."
Dynamic Class Initialization Semantics: A Jinja Extension
Susannah Mansky and Elsa L. Gunter (University of Illinois at UrbanaChampaign, USA) The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Javalevel bigstep and smallstep semantics, JVMlevel smallstep semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and reprove related proofs, including Javalevel type safety, equivalence between Javalevel bigstep and smallstep semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification. @InProceedings{CPP19p209, author = {Susannah Mansky and Elsa L. Gunter}, title = {Dynamic Class Initialization Semantics: A Jinja Extension}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {209221}, doi = {10.1145/3293880.3294104}, year = {2019}, } Publisher's Version Article Search 

Honoré, Wolf 
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Liyao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA) We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by lowlevel buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. @InProceedings{CPP19p234, author = {Nicolas Koh and Yao Li and Yishuai Li and Liyao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {234248}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version Article Search 

Hutin, Rémi 
CPP '19: "Formal Verification of a Program ..."
Formal Verification of a Program Obfuscation Based on Mixed BooleanArithmetic Expressions
Sandrine Blazy and Rémi Hutin (University of Rennes, France; Inria, France; CNRS, France; IRISA, France) The insertion of expressions mixing arithmetic operators and bitwise boolean operators is a widespread protection of sensitive data in source programs. This recent advanced obfuscation technique is one of the less studied among program obfuscations even if it is commonly found in binary code. In this paper, we formally verify in Coq this data obfuscation. It operates over a generic notion of mixed booleanarithmetic expressions and on properties of bitwise operators operating over machine integers. Our obfuscation performs two kinds of program transformations: rewriting of expressions and insertion of modular inverses. To facilitate its proof of correctness, we define boolean semantic tables, a data structure inspired from truth tables. Our obfuscation is integrated into the CompCert formally verified compiler where it operates over Clight programs. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results. @InProceedings{CPP19p196, author = {Sandrine Blazy and Rémi Hutin}, title = {Formal Verification of a Program Obfuscation Based on Mixed BooleanArithmetic Expressions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {196208}, doi = {10.1145/3293880.3294103}, year = {2019}, } Publisher's Version Article Search Info 

Immler, Fabian 
CPP '19: "Smooth Manifolds and Types ..."
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
Fabian Immler and Bohua Zhan (Carnegie Mellon University, USA; Institute of Software at Chinese Academy of Sciences, China) We formalize the definition and basic properties of smooth manifolds in Isabelle/HOL. Concepts covered include partition of unity, tangent and cotangent spaces, and the fundamental theorem for line integrals. We also construct some concrete manifolds such as spheres and projective spaces. The formalization makes extensive use of the existing libraries for topology and analysis. The existing library for linear algebra is not flexible enough for our needs. We therefore set up the first systematic and large scale application of ``types to sets''. It allows us to automatically transform the existing (type based) library of linear algebra to one with explicit carrier sets. @InProceedings{CPP19p65, author = {Fabian Immler and Bohua Zhan}, title = {Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6577}, doi = {10.1145/3293880.3294093}, year = {2019}, } Publisher's Version Article Search 

Kaiser, Jonas 
CPP '19: "Autosubst 2: Reasoning with ..."
Autosubst 2: Reasoning with Multisorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser (Saarland University, Germany) Formalising metatheory in the Coq proof assistant is tedious as reasoning with binders without native support requires a lot of uninteresting technicalities. To relieve users from soproduced boilerplate, the Autosubst framework automates working with de Bruijn terms: For each annotated inductive type, Autosubst generates a corresponding instantiation operation for parallel substitutions and a decision procedure for assumptionfree substitution lemmas. However, Autosubst is implemented in Ltac, Coq's tactic language, and thus suffers from Ltac's limitations. In particular, Autosubst is restricted to Coq and unscoped, nonmutual inductive types with a single sort of variables. In this paper, we present a new version of Autosubst that overcomes these restrictions. Autosubst 2 is an external code generator, which translates secondorder HOAS specifications into potentially mutual inductive term sorts. We extend the equational theory of Autosubst to the case of mutual inductive sorts by combining the application of multiple parallel substitutions into exactly one instantiation operation for each sort, i.e. we parallelise substitutions to vector substitutions. The resulting equational theory is both simpler and more expressive than that of the original Autosubst framework and allows us to present an even more elegant proof of part A of the POPLMark challenge. @InProceedings{CPP19p166, author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser}, title = {Autosubst 2: Reasoning with Multisorted de Bruijn Terms and Vector Substitutions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {166180}, doi = {10.1145/3293880.3294101}, year = {2019}, } Publisher's Version Article Search Info 

Kirst, Dominik 
CPP '19: "On Synthetic Undecidability ..."
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka (Saarland University, Germany) We formalise the computational undecidability of validity, satisfiability, and provability of firstorder formulas following a synthetic approach based on the computation native to Coq's constructive type theory. Concretely, we consider Tarski and Kripke semantics as well as classical and intuitionistic natural deduction systems and provide compact manyone reductions from the Post correspondence problem (PCP). Moreover, developing a basic framework for synthetic computability theory in Coq, we formalise standard results concerning decidability, enumerability, and reducibility without reference to a concrete model of computation. For instance, we prove the equivalence of Post's theorem with Markov's principle and provide a convenient technique for establishing the enumerability of inductive predicates such as the considered proof systems and PCP. @InProceedings{CPP19p38, author = {Yannick Forster and Dominik Kirst and Gert Smolka}, title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3851}, doi = {10.1145/3293880.3294091}, year = {2019}, } Publisher's Version Article Search Info 

Koh, Nicolas 
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Liyao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA) We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by lowlevel buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. @InProceedings{CPP19p234, author = {Nicolas Koh and Yao Li and Yishuai Li and Liyao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {234248}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version Article Search 

LarcheyWendling, Dominique 
CPP '19: "Certified Undecidability of ..."
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Yannick Forster and Dominique LarcheyWendling (Saarland University, Germany; University of Lorraine, France; CNRS, France; LORIA, France) We formally prove the undecidability of entailment in intuitionistic linear logic in Coq. We reduce the Post correspondence problem (PCP) via binary stack machines and Minsky machines to intuitionistic linear logic. The reductions rely on several technically involved formalisations, amongst them a binary stack machine simulator for PCP, a verified lowlevel compiler for instructionbased languages and a soundness proof for intuitionistic linear logic with respect to trivial phase semantics. We exploit the computability of all functions definable in constructive type theory and thus do not have to rely on a concrete model of computation, enabling the reduction proofs to focus on correctness properties. @InProceedings{CPP19p104, author = {Yannick Forster and Dominique LarcheyWendling}, title = {Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {104117}, doi = {10.1145/3293880.3294096}, year = {2019}, } Publisher's Version Article Search Info 

Lewis, Robert Y. 
CPP '19: "A Formal Proof of Hensel's ..."
A Formal Proof of Hensel's Lemma over the padic Integers
Robert Y. Lewis (Vrije Universiteit Amsterdam, Netherlands) The field of padic numbers ℚ_{p} and the ring of padic integers ℤ_{p} are essential constructions of modern number theory. Hensel’s lemma, described by Gouvêa as the “most important algebraic property of the padic numbers,” shows the existence of roots of polynomials over ℤ_{p} provided an initial seed point. The theorem can be proved for the padics with significantly weaker hypotheses than for general rings. We construct ℚ_{p} and ℤ_{p} in the Lean proof assistant, with various associated algebraic properties, and formally prove a strong form of Hensel’s lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic. @InProceedings{CPP19p15, author = {Robert Y. Lewis}, title = {A Formal Proof of Hensel's Lemma over the padic Integers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1526}, doi = {10.1145/3293880.3294089}, year = {2019}, } Publisher's Version Article Search 

Li, Wenda 
CPP '19: "Counting Polynomial Roots ..."
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the BudanFourier Theorem
Wenda Li and Lawrence C. Paulson (University of Cambridge, UK) Many problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified rootcounting procedures in major proof assistants are mainly based on the classical Sturm theorem, which only counts distinct roots. In this paper, we have strengthened the rootcounting ability in Isabelle/HOL by first formally proving the BudanFourier theorem. Subsequently, based on Descartes' rule of signs and Taylor shift, we have provided a verified procedure to efficiently overapproximate the number of real roots within an interval, counting multiplicity. For counting multiple roots exactly, we have extended our previous formalisation of Sturm's theorem. Finally, we combine verified components in the developments above to improve our previous certified complexrootcounting procedures based on Cauchy indices. We believe those verified routines will be crucial for certifying programs and building tactics. @InProceedings{CPP19p52, author = {Wenda Li and Lawrence C. Paulson}, title = {Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the BudanFourier Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {5264}, doi = {10.1145/3293880.3294092}, year = {2019}, } Publisher's Version Article Search 

Li, Yao 
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Liyao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA) We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by lowlevel buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. @InProceedings{CPP19p234, author = {Nicolas Koh and Yao Li and Yishuai Li and Liyao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {234248}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version Article Search 

Li, Yishuai 
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Liyao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA) We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by lowlevel buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. @InProceedings{CPP19p234, author = {Nicolas Koh and Yao Li and Yishuai Li and Liyao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {234248}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version Article Search 

Lochmann, Alexander 
CPP '19: "Certified ACKBO ..."
Certified ACKBO
Alexander Lochmann and Christian Sternagel (University of Innsbruck, Austria) Term rewriting in the presence of associative and commutative function symbols constitutes a highly expressive model of computation, which is for example well suited to reason about parallel computations. However, it is well known that the standard notion of termination does not apply any more: any term rewrite system containing a commutativity rule is nonterminating. Thus, instead of adding ACrules to a rewrite system, we switch to the notion of ACtermination. ACtermination can for example be shown using ACcompatible reduction orders. One specific example of such an order is ACKBO. We present our Isabelle/HOL formalization of the ACKBO order. On an abstract level this gives us a mechanized proof of the fact that ACKBO is indeed an ACcompatible reduction order. Moreover, we integrated corresponding check functions into the verified certifier CeTA. This has the more practical consequence of enabling the machine certification of ACtermination proofs generated by automated termination tools. @InProceedings{CPP19p144, author = {Alexander Lochmann and Christian Sternagel}, title = {Certified ACKBO}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {144151}, doi = {10.1145/3293880.3294099}, year = {2019}, } Publisher's Version Article Search 

Manighetti, Matteo 
CPP '19: "A ProofTheoretic Approach ..."
A ProofTheoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller (Inria, France; LIX, France; École Polytechnique, France) When presented with a formula to prove, most theorem provers for classical firstorder logic process that formula following several steps, one of which is commonly called skolemization. That process eliminates quantifier alternation within formulas by extending the language of the underlying logic with new Skolem functions and by instantiating certain quantifiers with terms built using Skolem functions. In this paper, we address the problem of checking (i.e., certifying) proof evidence that involves Skolem terms. Our goal is to do such certification without using the mathematical concepts of modeltheoretic semantics (i.e., preservation of satisfiability) and choice principles (i.e., epsilon terms). Instead, our proof checking kernel is an implementation of Gentzen's sequent calculus, which directly supports quantifier alternation by using eigenvariables. We shall describe deskolemization as a mapping from clientside terms, used in proofs generated by theorem provers, into kernelside terms, used within our proof checking kernel. This mapping which associates skolemized terms to eigenvariables relies on using outer skolemization. We also point out that the removal of Skolem terms from a proof is influenced by the polarities given to propositional connectives. @InProceedings{CPP19p78, author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller}, title = {A ProofTheoretic Approach to Certifying Skolemization}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {7890}, doi = {10.1145/3293880.3294094}, year = {2019}, } Publisher's Version Article Search 

Mansky, Susannah 
CPP '19: "Dynamic Class Initialization ..."
Dynamic Class Initialization Semantics: A Jinja Extension
Susannah Mansky and Elsa L. Gunter (University of Illinois at UrbanaChampaign, USA) The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Javalevel bigstep and smallstep semantics, JVMlevel smallstep semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and reprove related proofs, including Javalevel type safety, equivalence between Javalevel bigstep and smallstep semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification. @InProceedings{CPP19p209, author = {Susannah Mansky and Elsa L. Gunter}, title = {Dynamic Class Initialization Semantics: A Jinja Extension}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {209221}, doi = {10.1145/3293880.3294104}, year = {2019}, } Publisher's Version Article Search 

Mansky, William 
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Liyao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA) We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by lowlevel buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. @InProceedings{CPP19p234, author = {Nicolas Koh and Yao Li and Yishuai Li and Liyao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {234248}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version Article Search 

Middeldorp, Aart 
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear VariableSeparated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp (University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria) It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variableseparated rewrite systems. To this end, we formalize procedures for ground tree transducers and socalled RR_{n} relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the firstorder theory of ground rewriting for linear, variableseparated rewrite systems. It forms the basis for a formalized confluence checker for leftlinear, rightground systems. @InProceedings{CPP19p132, author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp}, title = {A Verified Ground Confluence Tool for Linear VariableSeparated Rewrite Systems in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {132143}, doi = {10.1145/3293880.3294098}, year = {2019}, } Publisher's Version Article Search 

Miller, Dale 
CPP '19: "A ProofTheoretic Approach ..."
A ProofTheoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller (Inria, France; LIX, France; École Polytechnique, France) When presented with a formula to prove, most theorem provers for classical firstorder logic process that formula following several steps, one of which is commonly called skolemization. That process eliminates quantifier alternation within formulas by extending the language of the underlying logic with new Skolem functions and by instantiating certain quantifiers with terms built using Skolem functions. In this paper, we address the problem of checking (i.e., certifying) proof evidence that involves Skolem terms. Our goal is to do such certification without using the mathematical concepts of modeltheoretic semantics (i.e., preservation of satisfiability) and choice principles (i.e., epsilon terms). Instead, our proof checking kernel is an implementation of Gentzen's sequent calculus, which directly supports quantifier alternation by using eigenvariables. We shall describe deskolemization as a mapping from clientside terms, used in proofs generated by theorem provers, into kernelside terms, used within our proof checking kernel. This mapping which associates skolemized terms to eigenvariables relies on using outer skolemization. We also point out that the removal of Skolem terms from a proof is influenced by the polarities given to propositional connectives. @InProceedings{CPP19p78, author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller}, title = {A ProofTheoretic Approach to Certifying Skolemization}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {7890}, doi = {10.1145/3293880.3294094}, year = {2019}, } Publisher's Version Article Search 

Paulson, Lawrence C. 
CPP '19: "Counting Polynomial Roots ..."
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the BudanFourier Theorem
Wenda Li and Lawrence C. Paulson (University of Cambridge, UK) Many problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified rootcounting procedures in major proof assistants are mainly based on the classical Sturm theorem, which only counts distinct roots. In this paper, we have strengthened the rootcounting ability in Isabelle/HOL by first formally proving the BudanFourier theorem. Subsequently, based on Descartes' rule of signs and Taylor shift, we have provided a verified procedure to efficiently overapproximate the number of real roots within an interval, counting multiplicity. For counting multiple roots exactly, we have extended our previous formalisation of Sturm's theorem. Finally, we combine verified components in the developments above to improve our previous certified complexrootcounting procedures based on Cauchy indices. We believe those verified routines will be crucial for certifying programs and building tactics. @InProceedings{CPP19p52, author = {Wenda Li and Lawrence C. Paulson}, title = {Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the BudanFourier Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {5264}, doi = {10.1145/3293880.3294092}, year = {2019}, } Publisher's Version Article Search 

Pierce, Benjamin C. 
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Liyao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA) We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by lowlevel buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. @InProceedings{CPP19p234, author = {Nicolas Koh and Yao Li and Yishuai Li and Liyao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {234248}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version Article Search 

Prathamesh, T. V. H. 
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear VariableSeparated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp (University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria) It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variableseparated rewrite systems. To this end, we formalize procedures for ground tree transducers and socalled RR_{n} relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the firstorder theory of ground rewriting for linear, variableseparated rewrite systems. It forms the basis for a formalized confluence checker for leftlinear, rightground systems. @InProceedings{CPP19p132, author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp}, title = {A Verified Ground Confluence Tool for Linear VariableSeparated Rewrite Systems in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {132143}, doi = {10.1145/3293880.3294098}, year = {2019}, } Publisher's Version Article Search 

Rapp, Franziska 
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear VariableSeparated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp (University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria) It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variableseparated rewrite systems. To this end, we formalize procedures for ground tree transducers and socalled RR_{n} relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the firstorder theory of ground rewriting for linear, variableseparated rewrite systems. It forms the basis for a formalized confluence checker for leftlinear, rightground systems. @InProceedings{CPP19p132, author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp}, title = {A Verified Ground Confluence Tool for Linear VariableSeparated Rewrite Systems in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {132143}, doi = {10.1145/3293880.3294098}, year = {2019}, } Publisher's Version Article Search 

Ravindran, Binoy 
CPP '19: "Formally Verified Big Step ..."
Formally Verified Big Step Semantics out of x8664 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran (Virginia Tech, USA) This paper presents a methodology for generating formally proven equivalence theorems between decompiled x8664 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x8664 machine model containing small step semantics for 1625 instructions. Second, a decompilationintologic methodology supporting both x8664 assembly and machine code at large scale. This work enables blackbox binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safetycritical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machinelearned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floatingpoint instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code. @InProceedings{CPP19p181, author = {Ian Roessle and Freek Verbeek and Binoy Ravindran}, title = {Formally Verified Big Step Semantics out of x8664 Binaries}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {181195}, doi = {10.1145/3293880.3294102}, year = {2019}, } Publisher's Version Article Search 

Roessle, Ian 
CPP '19: "Formally Verified Big Step ..."
Formally Verified Big Step Semantics out of x8664 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran (Virginia Tech, USA) This paper presents a methodology for generating formally proven equivalence theorems between decompiled x8664 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x8664 machine model containing small step semantics for 1625 instructions. Second, a decompilationintologic methodology supporting both x8664 assembly and machine code at large scale. This work enables blackbox binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safetycritical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machinelearned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floatingpoint instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code. @InProceedings{CPP19p181, author = {Ian Roessle and Freek Verbeek and Binoy Ravindran}, title = {Formally Verified Big Step Semantics out of x8664 Binaries}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {181195}, doi = {10.1145/3293880.3294102}, year = {2019}, } Publisher's Version Article Search 

Schäfer, Steven 
CPP '19: "Autosubst 2: Reasoning with ..."
Autosubst 2: Reasoning with Multisorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser (Saarland University, Germany) Formalising metatheory in the Coq proof assistant is tedious as reasoning with binders without native support requires a lot of uninteresting technicalities. To relieve users from soproduced boilerplate, the Autosubst framework automates working with de Bruijn terms: For each annotated inductive type, Autosubst generates a corresponding instantiation operation for parallel substitutions and a decision procedure for assumptionfree substitution lemmas. However, Autosubst is implemented in Ltac, Coq's tactic language, and thus suffers from Ltac's limitations. In particular, Autosubst is restricted to Coq and unscoped, nonmutual inductive types with a single sort of variables. In this paper, we present a new version of Autosubst that overcomes these restrictions. Autosubst 2 is an external code generator, which translates secondorder HOAS specifications into potentially mutual inductive term sorts. We extend the equational theory of Autosubst to the case of mutual inductive sorts by combining the application of multiple parallel substitutions into exactly one instantiation operation for each sort, i.e. we parallelise substitutions to vector substitutions. The resulting equational theory is both simpler and more expressive than that of the original Autosubst framework and allows us to present an even more elegant proof of part A of the POPLMark challenge. @InProceedings{CPP19p166, author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser}, title = {Autosubst 2: Reasoning with Multisorted de Bruijn Terms and Vector Substitutions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {166180}, doi = {10.1145/3293880.3294101}, year = {2019}, } Publisher's Version Article Search Info CPP '19: "CallByPushValue in Coq: ..." CallByPushValue in Coq: Operational, Equational, and Denotational Theory Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark (Saarland University, Germany) Callbypushvalue (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both callbyvalue (CBV) and callbyname (CBN). We formalise weak and strong operational semantics for (effectfree) CBPV, define its equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full λcalculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs. @InProceedings{CPP19p118, author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark}, title = {CallByPushValue in Coq: Operational, Equational, and Denotational Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {118131}, doi = {10.1145/3293880.3294097}, year = {2019}, } Publisher's Version Article Search Info 

Schlichtkrull, Anders 
CPP '19: "A Verified Prover Based on ..."
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel (DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland) The superposition calculus, which underlies firstorder theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional firstorder ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for firstorder logic. @InProceedings{CPP19p152, author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel}, title = {A Verified Prover Based on Ordered Resolution}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {152165}, doi = {10.1145/3293880.3294100}, year = {2019}, } Publisher's Version Article Search 

Smolka, Gert 
CPP '19: "On Synthetic Undecidability ..."
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka (Saarland University, Germany) We formalise the computational undecidability of validity, satisfiability, and provability of firstorder formulas following a synthetic approach based on the computation native to Coq's constructive type theory. Concretely, we consider Tarski and Kripke semantics as well as classical and intuitionistic natural deduction systems and provide compact manyone reductions from the Post correspondence problem (PCP). Moreover, developing a basic framework for synthetic computability theory in Coq, we formalise standard results concerning decidability, enumerability, and reducibility without reference to a concrete model of computation. For instance, we prove the equivalence of Post's theorem with Markov's principle and provide a convenient technique for establishing the enumerability of inductive predicates such as the considered proof systems and PCP. @InProceedings{CPP19p38, author = {Yannick Forster and Dominik Kirst and Gert Smolka}, title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3851}, doi = {10.1145/3293880.3294091}, year = {2019}, } Publisher's Version Article Search Info 

Sozeau, Matthieu 
CPP '19: "Eliminating Reflection from ..."
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau (Inria, France) Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although typechecking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda. The actual objects that can be checked are not proofterms, but derivations of proofterms. This suggests that any derivation of ETT can be translated into a typecheckable proof term of intensional type theory (ITT). However, this result, investigated categorically by Hofmann in 1995, and 10 years later more syntactically by Oury, has never given rise to an effective translation. In this paper, we provide the first effective syntactical translation from ETT to ITT with uniqueness of identity proofs and functional extensionality. This translation has been defined and proven correct in Coq and yields an executable plugin that translates a derivation in ETT into an actual Coq typing judgment. Additionally, we show how this result is extended in the context of homotopy type theory to a twolevel type theory. @InProceedings{CPP19p91, author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau}, title = {Eliminating Reflection from Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {91103}, doi = {10.1145/3293880.3294095}, year = {2019}, } Publisher's Version Article Search 

Spies, Simon 
CPP '19: "CallByPushValue in Coq: ..."
CallByPushValue in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark (Saarland University, Germany) Callbypushvalue (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both callbyvalue (CBV) and callbyname (CBN). We formalise weak and strong operational semantics for (effectfree) CBPV, define its equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full λcalculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs. @InProceedings{CPP19p118, author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark}, title = {CallByPushValue in Coq: Operational, Equational, and Denotational Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {118131}, doi = {10.1145/3293880.3294097}, year = {2019}, } Publisher's Version Article Search Info 

Stark, Kathrin 
CPP '19: "Autosubst 2: Reasoning with ..."
Autosubst 2: Reasoning with Multisorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser (Saarland University, Germany) Formalising metatheory in the Coq proof assistant is tedious as reasoning with binders without native support requires a lot of uninteresting technicalities. To relieve users from soproduced boilerplate, the Autosubst framework automates working with de Bruijn terms: For each annotated inductive type, Autosubst generates a corresponding instantiation operation for parallel substitutions and a decision procedure for assumptionfree substitution lemmas. However, Autosubst is implemented in Ltac, Coq's tactic language, and thus suffers from Ltac's limitations. In particular, Autosubst is restricted to Coq and unscoped, nonmutual inductive types with a single sort of variables. In this paper, we present a new version of Autosubst that overcomes these restrictions. Autosubst 2 is an external code generator, which translates secondorder HOAS specifications into potentially mutual inductive term sorts. We extend the equational theory of Autosubst to the case of mutual inductive sorts by combining the application of multiple parallel substitutions into exactly one instantiation operation for each sort, i.e. we parallelise substitutions to vector substitutions. The resulting equational theory is both simpler and more expressive than that of the original Autosubst framework and allows us to present an even more elegant proof of part A of the POPLMark challenge. @InProceedings{CPP19p166, author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser}, title = {Autosubst 2: Reasoning with Multisorted de Bruijn Terms and Vector Substitutions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {166180}, doi = {10.1145/3293880.3294101}, year = {2019}, } Publisher's Version Article Search Info CPP '19: "CallByPushValue in Coq: ..." CallByPushValue in Coq: Operational, Equational, and Denotational Theory Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark (Saarland University, Germany) Callbypushvalue (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both callbyvalue (CBV) and callbyname (CBN). We formalise weak and strong operational semantics for (effectfree) CBPV, define its equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full λcalculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs. @InProceedings{CPP19p118, author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark}, title = {CallByPushValue in Coq: Operational, Equational, and Denotational Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {118131}, doi = {10.1145/3293880.3294097}, year = {2019}, } Publisher's Version Article Search Info 

Sternagel, Christian 
CPP '19: "Certified ACKBO ..."
Certified ACKBO
Alexander Lochmann and Christian Sternagel (University of Innsbruck, Austria) Term rewriting in the presence of associative and commutative function symbols constitutes a highly expressive model of computation, which is for example well suited to reason about parallel computations. However, it is well known that the standard notion of termination does not apply any more: any term rewrite system containing a commutativity rule is nonterminating. Thus, instead of adding ACrules to a rewrite system, we switch to the notion of ACtermination. ACtermination can for example be shown using ACcompatible reduction orders. One specific example of such an order is ACKBO. We present our Isabelle/HOL formalization of the ACKBO order. On an abstract level this gives us a mechanized proof of the fact that ACKBO is indeed an ACcompatible reduction order. Moreover, we integrated corresponding check functions into the verified certifier CeTA. This has the more practical consequence of enabling the machine certification of ACtermination proofs generated by automated termination tools. @InProceedings{CPP19p144, author = {Alexander Lochmann and Christian Sternagel}, title = {Certified ACKBO}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {144151}, doi = {10.1145/3293880.3294099}, year = {2019}, } Publisher's Version Article Search 

Tabareau, Nicolas 
CPP '19: "Eliminating Reflection from ..."
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau (Inria, France) Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although typechecking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda. The actual objects that can be checked are not proofterms, but derivations of proofterms. This suggests that any derivation of ETT can be translated into a typecheckable proof term of intensional type theory (ITT). However, this result, investigated categorically by Hofmann in 1995, and 10 years later more syntactically by Oury, has never given rise to an effective translation. In this paper, we provide the first effective syntactical translation from ETT to ITT with uniqueness of identity proofs and functional extensionality. This translation has been defined and proven correct in Coq and yields an executable plugin that translates a derivation in ETT into an actual Coq typing judgment. Additionally, we show how this result is extended in the context of homotopy type theory to a twolevel type theory. @InProceedings{CPP19p91, author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau}, title = {Eliminating Reflection from Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {91103}, doi = {10.1145/3293880.3294095}, year = {2019}, } Publisher's Version Article Search 

Traytel, Dmitriy 
CPP '19: "A Verified Prover Based on ..."
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel (DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland) The superposition calculus, which underlies firstorder theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional firstorder ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for firstorder logic. @InProceedings{CPP19p152, author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel}, title = {A Verified Prover Based on Ordered Resolution}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {152165}, doi = {10.1145/3293880.3294100}, year = {2019}, } Publisher's Version Article Search 

Verbeek, Freek 
CPP '19: "Formally Verified Big Step ..."
Formally Verified Big Step Semantics out of x8664 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran (Virginia Tech, USA) This paper presents a methodology for generating formally proven equivalence theorems between decompiled x8664 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x8664 machine model containing small step semantics for 1625 instructions. Second, a decompilationintologic methodology supporting both x8664 assembly and machine code at large scale. This work enables blackbox binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safetycritical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machinelearned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floatingpoint instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code. @InProceedings{CPP19p181, author = {Ian Roessle and Freek Verbeek and Binoy Ravindran}, title = {Formally Verified Big Step Semantics out of x8664 Binaries}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {181195}, doi = {10.1145/3293880.3294102}, year = {2019}, } Publisher's Version Article Search 

Winterhalter, Théo 
CPP '19: "Eliminating Reflection from ..."
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau (Inria, France) Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although typechecking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda. The actual objects that can be checked are not proofterms, but derivations of proofterms. This suggests that any derivation of ETT can be translated into a typecheckable proof term of intensional type theory (ITT). However, this result, investigated categorically by Hofmann in 1995, and 10 years later more syntactically by Oury, has never given rise to an effective translation. In this paper, we provide the first effective syntactical translation from ETT to ITT with uniqueness of identity proofs and functional extensionality. This translation has been defined and proven correct in Coq and yields an executable plugin that translates a derivation in ETT into an actual Coq typing judgment. Additionally, we show how this result is extended in the context of homotopy type theory to a twolevel type theory. @InProceedings{CPP19p91, author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau}, title = {Eliminating Reflection from Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {91103}, doi = {10.1145/3293880.3294095}, year = {2019}, } Publisher's Version Article Search 

Xia, Liyao 
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Liyao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA) We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by lowlevel buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. @InProceedings{CPP19p234, author = {Nicolas Koh and Yao Li and Yishuai Li and Liyao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {234248}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version Article Search 

Ye, Qianchuan 
CPP '19: "A Verified Protocol Buffer ..."
A Verified Protocol Buffer Compiler
Qianchuan Ye and Benjamin Delaware (Purdue University, USA) The code responsible for serializing and deserializing untrusted external data is a vital component of any software that communicates with the outside world, as any bugs in these components can compromise the entire system. This is particularly true for verified systems which rely on trusted code to process external data, as any defects in the parsing code can invalidate any formal proofs about the system. One way to reduce the trusted code base of these systems is to use interface generators like Protocol Buffer and ASN.1 to generate serializers and deserializers from data descriptors. Of course, these generators are not immune to bugs. In this work, we formally verify a compiler for a realistic subset of the popular Protocol Buffer serialization format using the Coq proof assistant, proving once and for all the correctness of every generated serializer and deserializer. One of the challenges we had to overcome was the extreme flexibility of the Protocol Buffer format: the same source data can be encoded in an infinite number of ways, and the deserializer must faithfully recover the original source value from each. We have validated our verified system using the official conformance tests. @InProceedings{CPP19p222, author = {Qianchuan Ye and Benjamin Delaware}, title = {A Verified Protocol Buffer Compiler}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {222233}, doi = {10.1145/3293880.3294105}, year = {2019}, } Publisher's Version Article Search Artifacts Available 

Zdancewic, Steve 
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Liyao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA) We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by lowlevel buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. @InProceedings{CPP19p234, author = {Nicolas Koh and Yao Li and Yishuai Li and Liyao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {234248}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version Article Search 

Zhan, Bohua 
CPP '19: "Smooth Manifolds and Types ..."
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
Fabian Immler and Bohua Zhan (Carnegie Mellon University, USA; Institute of Software at Chinese Academy of Sciences, China) We formalize the definition and basic properties of smooth manifolds in Isabelle/HOL. Concepts covered include partition of unity, tangent and cotangent spaces, and the fundamental theorem for line integrals. We also construct some concrete manifolds such as spheres and projective spaces. The formalization makes extensive use of the existing libraries for topology and analysis. The existing library for linear algebra is not flexible enough for our needs. We therefore set up the first systematic and large scale application of ``types to sets''. It allows us to automatically transform the existing (type based) library of linear algebra to one with explicit carrier sets. @InProceedings{CPP19p65, author = {Fabian Immler and Bohua Zhan}, title = {Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6577}, doi = {10.1145/3293880.3294093}, year = {2019}, } Publisher's Version Article Search 
50 authors
proc time: 2.98