FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

This page contains an index consisting of author-provided keywords.

A
ABNF	A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Abstract Interpretation	The Map Equality Domain
ACL2	A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Architecture	Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Arithmetic	Extending VIAP to Handle Array Programs
Array	Extending VIAP to Handle Array Programs
Automatic Program Verification	Extending VIAP to Handle Array Programs
B
binarized neural networks	Verification of Binarized Neural Networks via Inter-Neuron Factoring
bounded model-checking	Lattice-Based Refinement in Bounded Model Checking
C
CakeML	Verified Certificate Checking for Counting Votes
certificate checking	Verified Certificate Checking for Counting Votes
Certifying Compilation	TWAM: A Certifying Abstract Machine for Logic Programs
concurrency	Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment
constrained rewriting	Loop Detection by Logically Constrained Term Rewriting
Coq	A Java bytecode formalisation
Correctness proofs	Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
counterexamples	Executable Counterexamples in Software Model Checking
D
data flow	A Tree-Based Approach to Data Flow Proofs
Deductive verification	Practical Methods for Reasoning about Java 8's Functional Programming Features
E
Ethereum	Towards verification of Ethereum smart contracts: a formalization of core of Solidity
Executable Harnesses	Executable Counterexamples in Software Model Checking
F
first-order logic	Extending VIAP to Handle Array Programs
Formal Methods	Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Formalisation	Verified Certificate Checking for Counting Votes
function summaries	Lattice-Based Refinement in Bounded Model Checking
functional programming	Practical Methods for Reasoning about Java 8's Functional Programming Features
G
grammar	A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
H
hardness of approximation	Verification of Binarized Neural Networks via Inter-Neuron Factoring
HOL	Verified Certificate Checking for Counting Votes
J
Java	Practical Methods for Reasoning about Java 8's Functional Programming Features
Java byte-code	A Java bytecode formalisation
JML	Practical Methods for Reasoning about Java 8's Functional Programming Features
L
lattice	Lattice-Based Refinement in Bounded Model Checking
lattice traversal	Lattice-Based Refinement in Bounded Model Checking
loops	Loop Detection by Logically Constrained Term Rewriting
low-level language	A Java bytecode formalisation
M
MapReduce framework	Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Mathematical Induction	Extending VIAP to Handle Array Programs
memory consistency models	Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment
ML	Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
Multi-dimensional	Extending VIAP to Handle Array Programs
N
Nested	Extending VIAP to Handle Array Programs
nontermination	Loop Detection by Logically Constrained Term Rewriting
O
OpenJML	Practical Methods for Reasoning about Java 8's Functional Programming Features
P
parsing	A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Privacy by design	Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Program Debugging	Executable Counterexamples in Software Model Checking
program transformation	Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Program Verification	Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications Verified Certificate Checking for Counting Votes A Tree-Based Approach to Data Flow Proofs
Prolog	TWAM: A Certifying Abstract Machine for Logic Programs
Proof-Producing Compilation	TWAM: A Certifying Abstract Machine for Logic Programs
R
Recurrences	Extending VIAP to Handle Array Programs
Relational Equivalence Verification	Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
S
Security	SideTrail: Verifying Time-Balancing of Cryptosystems
semantics	Towards verification of Ethereum smart contracts: a formalization of core of Solidity Formalising Executable Specifications of Low-Level Systems
side-channels	SideTrail: Verifying Time-Balancing of Cryptosystems
Single Transferable Vote scheme	Verified Certificate Checking for Counting Votes
Smart contracts	Towards verification of Ethereum smart contracts: a formalization of core of Solidity
SMT	Extending VIAP to Handle Array Programs
SMT solvers	Lattice-Based Refinement in Bounded Model Checking
Software Model Checking	Executable Counterexamples in Software Model Checking
software model-checking	Lattice-Based Refinement in Bounded Model Checking
Solidity	Towards verification of Ethereum smart contracts: a formalization of core of Solidity
Static Analysis	The Map Equality Domain
store buffer reduction	Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment
T
theorem proving	Verified Certificate Checking for Counting Votes Formalising Executable Specifications of Low-Level Systems
theory	Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment
theory of arrays	The Map Equality Domain
tree automata	A Tree-Based Approach to Data Flow Proofs
type systems	Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
type theory	Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
V
Verification	Verification of Binarized Neural Networks via Inter-Neuron Factoring SideTrail: Verifying Time-Balancing of Cryptosystems A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars Formalising Executable Specifications of Low-Level Systems
W
Warren Abstract Machine	TWAM: A Certifying Abstract Machine for Logic Programs

Disclaimer | Powered by EasyChair Smart Program