| no |
title |
author |
magazine |
year |
volume |
issue |
page(s) |
type |
| 1 |
A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines
|
Neider, Daniel
|
|
|
|
7 |
p. 1523-1552
|
article
|
| 2 |
Automata Terms in a Lazy WSkS Decision Procedure
|
Havlena, Vojtěch
|
|
|
|
7 |
p. 971-999
|
article
|
| 3 |
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
|
Bryant, Randal E.
|
|
|
|
7 |
p. 1361-1391
|
article
|
| 4 |
Constructive Decision via Redundancy-Free Proof-Search
|
Larchey-Wendling, Dominique
|
|
|
|
7 |
p. 1197-1219
|
article
|
| 5 |
Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant
|
Popescu, Andrei
|
|
|
|
7 |
p. 1027-1070
|
article
|
| 6 |
Fine-Grained Complexity of Safety Verification
|
Chini, Peter
|
|
|
|
7 |
p. 1419-1444
|
article
|
| 7 |
Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
|
Schlichtkrull, Anders
|
|
|
|
7 |
p. 1169-1195
|
article
|
| 8 |
From QBFs to MALL and Back via Focussing
|
Das, Anupam
|
|
|
|
7 |
p. 1221-1245
|
article
|
| 9 |
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs
|
Champion, Adrien
|
|
|
|
7 |
p. 1393-1418
|
article
|
| 10 |
Model Completeness, Uniform Interpolants and Superposition Calculus
|
Calvanese, Diego
|
|
|
|
7 |
p. 941-969
|
article
|
| 11 |
Multi-cost Bounded Tradeoff Analysis in MDP
|
Hartmanns, Arnd
|
|
|
|
7 |
p. 1483-1522
|
article
|
| 12 |
Natural Projection as Partial Model Checking
|
Costa, Gabriele
|
|
|
|
7 |
p. 1445-1481
|
article
|
| 13 |
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers
|
Trentin, Patrick
|
|
|
|
7 |
p. 1071-1096
|
article
|
| 14 |
Parameterized Model Checking on the TSO Weak Memory Model
|
Conchon, Sylvain
|
|
|
|
7 |
p. 1307-1330
|
article
|
| 15 |
Preface: Special Issue of Selected Extended Papers from IJCAR 2018
|
Galmiche, Didier
|
|
|
|
7 |
p. 1165-1167
|
article
|
| 16 |
Preface: Special Issue of Selected Extended Papers of CADE 2019
|
Fontaine, Pascal
|
|
|
|
7 |
p. 891-892
|
article
|
| 17 |
Probably Partially True: Satisfiability for Łukasiewicz Infinitely-Valued Probabilistic Logic and Related Topics
|
Finger, Marcelo
|
|
|
|
7 |
p. 1269-1286
|
article
|
| 18 |
Proof-Producing Synthesis of CakeML from Monadic HOL Functions
|
Abrahamsson, Oskar
|
|
|
|
7 |
p. 1287-1306
|
article
|
| 19 |
Selected and Extended Papers from TACAS 2018: Preface
|
Beyer, Dirk
|
|
|
|
7 |
p. 1331-1332
|
article
|
| 20 |
Simulating Strong Practical Proof Systems with Extended Resolution
|
Kiesl, Benjamin
|
|
|
|
7 |
p. 1247-1267
|
article
|
| 21 |
Superposition with Lambdas
|
Bentkamp, Alexander
|
|
|
|
7 |
p. 893-940
|
article
|
| 22 |
Synthesizing Precise and Useful Commutativity Conditions
|
Bansal, Kshitij
|
|
|
|
7 |
p. 1333-1359
|
article
|
| 23 |
Towards Satisfiability Modulo Parametric Bit-vectors
|
Niemetz, Aina
|
|
|
|
7 |
p. 1001-1025
|
article
|
Journal description