FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Approximation	The next 10^4 UppSAT Approximations (PDF, talk)
automated reasonning	Centralizing Equality Reasoning in MCSAT (PDF, talk)
B
Blockchain	SMT-based Compile-time Verification of Safety Properties for Smart Contracts (PDF, talk)
C
Constrained Horn Clauses	Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
D
Deductive programs verification	Alt-Ergo 2.2 (PDF, talk)
E
Egraph	Centralizing Equality Reasoning in MCSAT (PDF, talk)
Ethereum	SMT-based Compile-time Verification of Safety Properties for Smart Contracts (PDF, talk)
F
first-order logic	What is the Point of an SMT-LIB Problem? (PDF, talk)
Fixed Point Arithmetic	The next 10^4 UppSAT Approximations (PDF, talk)
Floating Point Arithmetic	The next 10^4 UppSAT Approximations (PDF, talk)
formal verification	SMT-based Compile-time Verification of Safety Properties for Smart Contracts (PDF, talk)
H
higher-order logic	Higher-Order SMT Solving (PDF, talk)
I
ic3	Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
Inductive invariants	Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
instantiation	Higher-Order SMT Solving (PDF, talk)
K
Knapsack	Puli - A Problem-Specific OMT Solver (PDF, talk)
L
Linearization	The next 10^4 UppSAT Approximations (PDF, talk)
M
MC-SAT	Centralizing Equality Reasoning in MCSAT (PDF, talk)
O
OMT	Puli - A Problem-Specific OMT Solver (PDF, talk)
P
PDR	Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
polymorphism	Alt-Ergo 2.2 (PDF, talk)
Program Verification	Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
property directed reachability	Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
Q
quantifier instantiation	Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
quantifiers	Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
R
Real Arithetmic	The next 10^4 UppSAT Approximations (PDF, talk)
Rewrite Rules	Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk)
rewriting	SMT Solving Modulo Tableau and Rewriting Theories (PDF, talk)
S
Safety properties	SMT-based Compile-time Verification of Safety Properties for Smart Contracts (PDF, talk)
SAT	SMT Solving Modulo Tableau and Rewriting Theories (PDF, talk)
Satisfiablity Modulo Theories	Alt-Ergo 2.2 (PDF, talk)
Smart contracts	SMT-based Compile-time Verification of Safety Properties for Smart Contracts (PDF, talk)
SMT	The next 10^4 UppSAT Approximations (PDF, talk) Puli - A Problem-Specific OMT Solver (PDF, talk) SMT-based Compile-time Verification of Safety Properties for Smart Contracts (PDF, talk) Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk) Higher-Order SMT Solving (PDF, talk) SMT Solving Modulo Tableau and Rewriting Theories (PDF, talk) What is the Point of an SMT-LIB Problem? (PDF, talk)
SMT-solving	Centralizing Equality Reasoning in MCSAT (PDF, talk)
superposition	SMT Solving Modulo Tableau and Rewriting Theories (PDF, talk)
Syntax-Guided Synthesis	Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk)
T
tableaux	SMT Solving Modulo Tableau and Rewriting Theories (PDF, talk)
theorem proving	What is the Point of an SMT-LIB Problem? (PDF, talk)
W
WSN	Puli - A Problem-Specific OMT Solver (PDF, talk)

Disclaimer | Powered by EasyChair Smart Program