2,199 papers · page 10 of 110
Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler
We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained determinized program satisfies a given quantitative specification, i.e., bounds on e…
Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, Georg Zetzsche
We study Satisfiability Modulo Theories (SMT) enriched with the so-called Ramsey quantifiers, which assert the existence of cliques (complete graphs) in the graph induced by some formulas. The extended framework is known to have applications in proving program termination (in par…
Mikolaj Bojanczyk, Bartek Klin
We consider injective first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order interpretation can use a k-tuple of input nodes to represent a single output node. We prove that the equiv…
Michael Borkowski, Niki Vazou, Ranjit Jhala
Practical checkers based on refinement types use the combination of implicit semantic subtyping and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal metatheoretic accounting of the sound…
Ian Briggs, Yash Lad, Pavel Panchekha
Achieving speed and accuracy for math library functions like exp, sin, and log is difficult. This is because low-level implementation languages like C do not help math library developers catch mathematical errors, build implementations incrementally, or separate high-level and lo…
Alex Buna-Marginean, Vincent Cheval, Mahsa Shirmohammadi, James Worrell
We introduce the class of P-finite automata. These are a generalisation of weighted automata, in which the weights of transitions can depend polynomially on the length of the input word. P-finite automata can also be viewed as simple tail-recursive programs in which the arguments…
Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, Caterina Urban
It is widely known that the precision of a program analyzer is closely related to intensional program properties, namely, properties concerning how the program is written. This explains, for instance, the interest in code obfuscation techniques, namely, tools explicitly designed …
John Peter Campora III, Mohammad Wahiduzzaman Khan, Sheng Chen
Gradual typing has emerged as a popular design point in programming languages, attracting significant interests from both academia and industry. Programmers in gradually typed languages are free to utilize static and dynamic typing as needed. To make such languages sound, runtime…
Jacques Carette, Chris Heunen, Robin Kaarsgaard, Amr Sabry
Rig groupoids provide a semantic model of Π, a universal classical reversible programming language over finite types. We prove that extending rig groupoids with just two maps and three equations about them results in a model of quantum computing that is computationally universal …
Giuseppe Castagna, Mickaël Laurent, Kim Nguyen
We present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types, and subtyping, and prove its safety. We then define a type reconstruction algorithm that is sound and terminating. This yields a system in which unannotated…
Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, Gabriele Tedeschi
Past years have seen the development of a few proposals for quantum extensions of process calculi. The rationale is clear: with the development of quantum communication protocols, there is a need to abstract and focus on the basic features of quantum concurrent systems, like CCS …
Soham Chakraborty, Shankara Narayanan Krishna, Umang Mathur, Andreas Pavlogiannis
Weak-memory models are standard formal specifications of concurrency across hardware, programming languages, and distributed systems. A fundamental computational problem is consistency testing: is the observed execution of a concurrent program in alignment with the specification …
Nicolas Chataing, Stephen Dolan, Gabriel Scherer, Jeremy Yallop
We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument. Unboxing must be statically rejected when it could introduce conf…
Joshua M. Cohen, Philip Johnson-Freyd
Intermediate verification languages like Why3 and Boogie have made it much easier to build program verifiers, transforming the process into a logic compilation problem rather than a proof automation one. Why3 in particular implements a rich logic for program specification with po…
Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe
Cyclic proof systems, in which induction is managed implicitly, are a promising approach to automatic verification. The soundness of cyclic proof graphs is ensured by checking them against a trace-based Infinite Descent property. Although the problem of checking Infinite Descent …
Patrick Cousot
We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a natural relational semantics covering both…
Will Crichton, Shriram Krishnamurthi
Passive documents and active programs now widely comingle. Document languages include Turing-complete programming elements, and programming languages include sophisticated document notations. However, there are no formal foundations that model these languages. This matters becaus…
John Cyphert, Zachary Kincaid
This paper presents a program analysis method that generates program summaries involving polynomial arithmetic. Our approach builds on prior techniques that use solvable polynomial maps for summarizing loops. These techniques are able to generate all polynomial invariants for a r…
Henry DeYoung, Andreia Mordido, Frank Pfenning, Ankush Das
We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this setting, we describe a notion of parametricity for type constructors and then exploit it to define paramet…
Haowei Deng, Runzhou Tao, Yuxiang Peng, Xiaodi Wu
Quantum programs are notoriously difficult to code and verify due to unintuitive quantum knowledge associated with quantum programming. Automated tools relieving the tedium and errors associated with low-level quantum details would hence be highly desirable. In this paper, we ini…