Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
alastairreid committed Jun 22, 2024
1 parent 0c2f7c7 commit b9ff752
Show file tree
Hide file tree
Showing 37 changed files with 1,266 additions and 2 deletions.
16 changes: 16 additions & 0 deletions _papers/dutertre:smt:2015.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
---
ENTRYTYPE: inproceedings
added: 2024-06-16
authors:
- Bruno Dutertre
booktitle: 13th International Workshop on Satisfiability Modulo Theories (SMT 2015)
layout: paper
month: July
read: false
readings: []
title: Solving Exists/Forall Problems With Yices
year: 2015
notes:
papers:
---
{% include links.html %}
12 changes: 10 additions & 2 deletions _papers/mosier:sandp:2023.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,9 @@ eprinttype: arXiv
journal: CoRR
layout: paper
link: https://doi.org/10.48550/arXiv.2309.05174
read: false
readings: []
read: true
readings:
- 2023-12-01
timestamp: Fri, 15 Sep 2023 12:26:52 +0200
title: 'Serberus: Protecting Cryptographic Code from Spectres at Compile-Time'
url: https://doi.org/10.48550/arXiv.2309.05174
Expand All @@ -27,4 +28,11 @@ notes:
- speculative execution
papers:
---

Serberus is a mitigation against [speculative execution] attacks
implemented as an extension of LLVM.
It relies on the use of Intel Architecture CET features to
constrain speculative branches.


{% include links.html %}
27 changes: 27 additions & 0 deletions _papers/sasnauskas:arxiv:2018.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
---
ENTRYTYPE: misc
added: 2024-06-16
archiveprefix: arXiv
authors:
- Raimondas Sasnauskas
- Yang Chen
- Peter Collingbourne
- Jeroen Ketema
- Gratian Lup
- Jubi Taneja
- John Regehr
eprint: '1711.04422'
layout: paper
primaryclass: id=\textquotesingle cs.PL\textquotesingle full\_name=\textquotesingle Programming Languages\textquotesingle is\_active=True alt\_name=None
in\_archive=\textquotesingle cs\textquotesingle is\_general=False description=\textquotesingle Covers programming language semantics, language features,
programming approaches (such as object-oriented programming, functional programming, logic programming). Also includes material on compilers oriented
towards programming languages; other material on compilers may be more appropriate in Architecture (AR). Roughly includes material in ACM Subject Classes
D.1 and D.3.\textquotesingle
read: false
readings: []
title: 'Souper: A Synthesizing Superoptimizer'
year: 2018
notes:
papers:
---
{% include links.html %}
31 changes: 31 additions & 0 deletions _staging/10.1007:978-3-030-29436-6_22.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
---
ENTRYTYPE: inproceedings
abstract: Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These approaches, however, cannot be used
directly to reason about bit-vectors of symbolic bit-width. To address this shortcoming, we propose a translation from bit-vector formulas with parametric
bit-width to formulas in a logic supported by SMT solvers that includes non-linear integer arithmetic, uninterpreted functions, and universal quantification.
While this logic is undecidable, this approach can still solve many formulas by capitalizing on advances in SMT solving for non-linear arithmetic and
universally quantified formulas. We provide several case studies in which we have applied this approach with promising results, including the bit-width
independent verification of invertibility conditions, compiler optimizations, and bit-vector rewrites.
added: 2024-06-22
address: Cham
authors:
- Aina Niemetz
- Mathias Preiner
- Andrew Reynolds
- Yoni Zohar
- Clark Barrett
- Cesare Tinelli
booktitle: Automated Deduction - CADE 27
editor: Fontaine, Pascal
isbn: 978-3-030-29436-6
layout: paper
pages: 366-384
publisher: Springer International Publishing
read: false
readings: []
title: Towards Bit-Width-Independent Proofs in SMT Solvers
year: 2019
notes:
papers:
---
{% include links.html %}
29 changes: 29 additions & 0 deletions _staging/10.1007:978-3-319-21668-3_10.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
---
ENTRYTYPE: inproceedings
abstract: Given a specification and a set of candidate programs (program space), the program synthesis problem is to find a candidate program that satisfies
the specification. We present the synthesis through unification (STUN) approach, which is an extension of the counter-example guided inductive synthesis
(CEGIS) approach. In CEGIS, the synthesizer maintains a subset S of inputs and a candidate program \textbackslash \textdollar \textbackslash \textdollar
\textbackslash backslashmathtt \textbackslash Prog\textbackslash \textbackslash \textdollar \textbackslash \textdollar that is correct for S. The synthesizer
repeatedly checks if there exists a counterexample input c such that the execution of \textbackslash \textdollar \textbackslash \textdollar \textbackslash
backslashmathtt \textbackslash Prog\textbackslash \textbackslash \textdollar \textbackslash \textdollar is incorrect on c. If so, the synthesizer enlarges
S to include c, and picks a program from the program space that is correct for the new set S.
added: 2024-06-22
address: Cham
authors:
- Rajeev Alur
- Pavol {\v C}erný
- Arjun Radhakrishna
booktitle: Computer Aided Verification
editor: Kroening, Daniel and P{\u a}s{\u a}reanu, Corina S.
isbn: 978-3-319-21668-3
layout: paper
pages: 163-179
publisher: Springer International Publishing
read: false
readings: []
title: Synthesis Through Unification
year: 2015
notes:
papers:
---
{% include links.html %}
34 changes: 34 additions & 0 deletions _staging/10.1007:978-3-319-96145-3_15.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
---
ENTRYTYPE: inproceedings
abstract: Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution
space, and tools often require a user-provided syntactic restriction of the search space. We propose a new approach to program synthesis that combines
the strengths of a counterexample-guided inductive synthesizer with those of a theory solver, exploring the solution space more efficiently without relying
on user guidance. We call this approach CEGIS(\textbackslash \textdollar \textbackslash \textdollar \textbackslash backslashmathcal \textbackslash T\textbackslash
\textbackslash \textdollar \textbackslash \textdollar T), where \textbackslash \textdollar \textbackslash \textdollar \textbackslash backslashmathcal
\textbackslash T\textbackslash \textbackslash \textdollar \textbackslash \textdollar Tis a first-order theory. In this paper, we focus on one particular
challenge for program synthesizers, namely the generation of programs that require non-trivial constants. This is a fundamentally difficult task for state-of-the-art
synthesizers. We present two exemplars, one based on Fourier-Motzkin (FM) variable elimination and one based on first-order satisfiability. We demonstrate
the practical value of CEGIS(\textbackslash \textdollar \textbackslash \textdollar \textbackslash backslashmathcal \textbackslash T\textbackslash \textbackslash
\textdollar \textbackslash \textdollar T) by automatically synthesizing programs for a set of intricate benchmarks.
added: 2024-06-22
address: Cham
authors:
- Alessandro Abate
- Cristina David
- Pascal Kesseli
- Daniel Kroening
- Elizabeth Polgreen
booktitle: Computer Aided Verification
editor: Chockler, Hana and Weissenbacher, Georg
isbn: 978-3-319-96145-3
layout: paper
pages: 270-288
publisher: Springer International Publishing
read: false
readings: []
title: Counterexample Guided Inductive Synthesis Modulo Theories
year: 2018
notes:
papers:
---
{% include links.html %}
23 changes: 23 additions & 0 deletions _staging/10.1007:978-3-642-54013-4_12.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
---
ENTRYTYPE: inproceedings
abstract: Compiler optimizations play an increasingly important role in code generation. This is especially true with the advent of resourcelimited mobile
devices. We rely on compiler optimizations to improve performance, reduce code size, and reduce power consumption of our programs.
added: 2024-06-22
address: Berlin, Heidelberg
authors:
- Nuno P. Lopes
- José Monteiro
booktitle: Verification, Model Checking, and Abstract Interpretation
editor: McMillan, Kenneth L. and Rival, Xavier
isbn: 978-3-642-54013-4
layout: paper
pages: 203-221
publisher: Springer Berlin Heidelberg
read: false
readings: []
title: Weakest Precondition Synthesis for Compiler Optimizations
year: 2014
notes:
papers:
---
{% include links.html %}
28 changes: 28 additions & 0 deletions _staging/10.1007:978-3-662-54577-5_18.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
---
ENTRYTYPE: inproceedings
abstract: Given a semantic constraint specified by a logical formula, and a syntactic constraint specified by a context-free grammar, the Syntax-Guided
Synthesis (SyGuS) problem is to find an expression that satisfies both the syntactic and semantic constraints. An enumerative approach to solve this problem
is to systematically generate all expressions from the syntactic space with some pruning, and has proved to be surprisingly competitive in the newly started
competition of SyGuS solvers. It performs well on small to medium sized benchmarks, produces succinct expressions, and has the ability to generalize from
input-output examples. However, its performance degrades drastically with the size of the smallest solution. To overcome this limitation, in this paper
we propose an alternative approach to solve SyGuS instances.
added: 2024-06-22
address: Berlin, Heidelberg
authors:
- Rajeev Alur
- Arjun Radhakrishna
- Abhishek Udupa
booktitle: Tools and Algorithms for the Construction and Analysis of Systems
editor: Legay, Axel and Margaria, Tiziana
isbn: 978-3-662-54577-5
layout: paper
pages: 319-336
publisher: Springer Berlin Heidelberg
read: false
readings: []
title: Scaling Enumerative Program Synthesis via Divide and Conquer
year: 2017
notes:
papers:
---
{% include links.html %}
38 changes: 38 additions & 0 deletions _staging/10.1007:s00236-017-0294-5.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
---
ENTRYTYPE: article
abstract: Formal synthesis is the process of generating a program satisfying a high-level formal specification. In recent times, effective formal synthesis
methods have been proposed based on the use of inductive learning. We refer to this class of methods that learn programs from examples as formal inductive
synthesis. In this paper, we present a theoretical framework for formal inductive synthesis. We discuss how formal inductive synthesis differs from traditional
machine learning. We then describe oracle-guided inductive synthesis (OGIS), a framework that captures a family of synthesizers that operate by iteratively
querying an oracle. An instance of OGIS that has had much practical impact is counterexample-guided inductive synthesis (CEGIS). We present a theoretical
characterization of CEGIS for learning any program that computes a recursive language. In particular, we analyze the relative power of CEGIS variants
where the types of counterexamples generated by the oracle varies. We also consider the impact of bounded versus unbounded memory available to the learning
algorithm. In the special case where the universe of candidate programs is finite, we relate the speed of convergence to the notion of teaching dimension
studied in machine learning theory. Altogether, the results of the paper take a first step towards a theoretical foundation for the emerging field of
formal inductive synthesis.
added: 2024-06-22
address: Berlin, Heidelberg
authors:
- Susmit Jha
- Sanjit A. Seshia
doi: 10.1007/s00236-017-0294-5
issn: 0001-5903
issue_date: November 2017
journal: Acta Inf.
layout: paper
link: https://doi.org/10.1007/s00236-017-0294-5
month: nov
number: '7'
numpages: '34'
pages: 693-726
publisher: Springer-Verlag
read: false
readings: []
title: A theory of formal synthesis via inductive learning
url: https://doi.org/10.1007/s00236-017-0294-5
volume: '54'
year: 2017
notes:
papers:
---
{% include links.html %}
37 changes: 37 additions & 0 deletions _staging/10.1145:1706299.1706345.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
---
ENTRYTYPE: inproceedings
abstract: We present an automated technique for generating compiler optimizations from examples of concrete programs before and after improvements have
been made to them. The key technical insight of our technique is that a proof of equivalence between the original and transformed concrete programs informs
us which aspects of the programs are important and which can be discarded. Our technique therefore uses these proofs, which can be produced by translation
validation or a proof-carrying compiler, as a guide to generalize the original and transformed programs into broadly applicable optimization rules.We
present a category-theoretic formalization of our proof generalization technique. This abstraction makes our technique applicable to logics besides our
own. In particular, we demonstrate how our technique can also be used to learn query optimizations for relational databases or to aid programmers in debugging
type errors.Finally, we show experimentally that our technique enables programmers to train a compiler with application-specific optimizations by providing
concrete examples of original programs and the desired transformed programs. We also show how it enables a compiler to learn efficient-to-run optimizations
from expensive-to-run super-optimizers.
added: 2024-06-22
address: New York, NY, USA
authors:
- Ross Tate
- Michael Stepp
- Sorin Lerner
booktitle: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
doi: 10.1145/1706299.1706345
isbn: '9781605584799'
keywords: proof generalization, explanation-based learning, compiler optimization
layout: paper
link: https://doi.org/10.1145/1706299.1706345
location: Madrid, Spain
numpages: '14'
pages: 389-402
publisher: Association for Computing Machinery
read: false
readings: []
series: POPL '10
title: Generating compiler optimizations from proofs
url: https://doi.org/10.1145/1706299.1706345
year: 2010
notes:
papers:
---
{% include links.html %}
39 changes: 39 additions & 0 deletions _staging/10.1145:1707801.1706345.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
---
ENTRYTYPE: article
abstract: We present an automated technique for generating compiler optimizations from examples of concrete programs before and after improvements have
been made to them. The key technical insight of our technique is that a proof of equivalence between the original and transformed concrete programs informs
us which aspects of the programs are important and which can be discarded. Our technique therefore uses these proofs, which can be produced by translation
validation or a proof-carrying compiler, as a guide to generalize the original and transformed programs into broadly applicable optimization rules.We
present a category-theoretic formalization of our proof generalization technique. This abstraction makes our technique applicable to logics besides our
own. In particular, we demonstrate how our technique can also be used to learn query optimizations for relational databases or to aid programmers in debugging
type errors.Finally, we show experimentally that our technique enables programmers to train a compiler with application-specific optimizations by providing
concrete examples of original programs and the desired transformed programs. We also show how it enables a compiler to learn efficient-to-run optimizations
from expensive-to-run super-optimizers.
added: 2024-06-22
address: New York, NY, USA
authors:
- Ross Tate
- Michael Stepp
- Sorin Lerner
doi: 10.1145/1707801.1706345
issn: 0362-1340
issue_date: January 2010
journal: SIGPLAN Not.
keywords: proof generalization, explanation-based learning, compiler optimization
layout: paper
link: https://doi.org/10.1145/1707801.1706345
month: jan
number: '1'
numpages: '14'
pages: 389-402
publisher: Association for Computing Machinery
read: false
readings: []
title: Generating compiler optimizations from proofs
url: https://doi.org/10.1145/1707801.1706345
volume: '45'
year: 2010
notes:
papers:
---
{% include links.html %}
37 changes: 37 additions & 0 deletions _staging/10.1145:1993316.1993532.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
---
ENTRYTYPE: article
abstract: Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three
years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every compiler we tested
was found to crash and also to silently generate wrong code when presented with valid input. In this paper we present our compiler-testing tool and the
results of our bug-hunting study. Our first contribution is to advance the state of the art in compiler testing. Unlike previous tools, Csmith generates
programs that cover a large subset of C while avoiding the undefined and unspecified behaviors that would destroy its ability to automatically find wrong-code
bugs. Our second contribution is a collection of qualitative and quantitative results about the bugs we have found in open-source C compilers.
added: 2024-06-22
address: New York, NY, USA
authors:
- Xuejun Yang
- Yang Chen
- Eric Eide
- John Regehr
doi: 10.1145/1993316.1993532
issn: 0362-1340
issue_date: June 2011
journal: SIGPLAN Not.
keywords: random testing, random program generation, compiler testing, compiler defect, automated testing
layout: paper
link: https://doi.org/10.1145/1993316.1993532
month: jun
number: '6'
numpages: '12'
pages: 283-294
publisher: Association for Computing Machinery
read: false
readings: []
title: Finding and understanding bugs in C compilers
url: https://doi.org/10.1145/1993316.1993532
volume: '46'
year: 2011
notes:
papers:
---
{% include links.html %}
Loading

0 comments on commit b9ff752

Please sign in to comment.