VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

A
abstract domain of polyhedra	A certifying frontend for (sub)polyhedral abstract domains
abstract interpretation	A certifying frontend for (sub)polyhedral abstract domains
algebraic data types	Formalizing Semantics with an Automatic Program Verifier
Artificial Intelligence	A Model for Capturing and Replaying Proof Strategies
Automated Program Verifiers	Formalizing Semantics with an Automatic Program Verifier
Automated theorem proving via SMT solver	Automatically verified implementation of data structures based on AVL trees (SHORT)
B
Balanced tree data structures	Automatically verified implementation of data structures based on AVL trees (SHORT)
C
C verification	Separation algebras for C verification in Coq
certification	Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
cloud computing	Formal Modeling and Verification of CloudProxy
Coq	Separation algebras for C verification in Coq
D
deductive verification	Automatically verified implementation of data structures based on AVL trees (SHORT)
E
efficient refinement check in VCC	Efficient Refinement Checking in VCC
Error Explanation	What Gives? A Hybrid Algorithm for Error Explanation
F
formal methods	A Model for Capturing and Replaying Proof Strategies
formal specification	Efficient Refinement Checking in VCC
Formal verification	A Verification Condition Visualizer
Formalization of Language Semantics	Formalizing Semantics with an Automatic Program Verifier
Framing	A logical analysis of framing for specifications with pure method calls
H
higher-order logic	Formalizing Semantics with an Automatic Program Verifier
Hoare logic	What Gives? A Hybrid Algorithm for Error Explanation
I
Inductive Reasoning	Formalizing Semantics with an Automatic Program Verifier
interactive theorem proving	Using Promela in a Fully Verified Executable LTL Model Checker (SHORT)
interpolants	What Gives? A Hybrid Algorithm for Error Explanation
Isabelle/HOL	Separation Kernel Verification: the XtratuM Case Study Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
J
Java	The KeY Platform for Verification and Analysis of Java Programs
K
kernel verification	Separation Kernel Verification: the XtratuM Case Study
L
Linking	A logical analysis of framing for specifications with pure method calls
Local reasoning	A logical analysis of framing for specifications with pure method calls
LTL	Using Promela in a Fully Verified Executable LTL Model Checker (SHORT)
M
MILS	Separation Kernel Verification: the XtratuM Case Study
Minimal Unsatisfiable Core	What Gives? A Hybrid Algorithm for Error Explanation
MMU	Store Buffer Reduction with MMUs
Model Checker	Using Promela in a Fully Verified Executable LTL Model Checker (SHORT)
model validation	Formal Modeling and Verification of CloudProxy
modeling	Formal Modeling and Verification of CloudProxy
N
Nontermination	Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
P
parameterized model checking	Model Checking Parameterized Timed Systems
program verification in Coq	A certifying frontend for (sub)polyhedral abstract domains
Proof Obligations	A Model for Capturing and Replaying Proof Strategies
Proof Patterns	A Model for Capturing and Replaying Proof Strategies
Pure method calls	A logical analysis of framing for specifications with pure method calls
R
real-time	Model Checking Parameterized Timed Systems
real-time verification	Timed Refinements for Verification of Real-Time Object Code Programs
refinement-based verification	Timed Refinements for Verification of Real-Time Object Code Programs
Region logic	A logical analysis of framing for specifications with pure method calls
S
Security	Formal Modeling and Verification of CloudProxy The KeY Platform for Verification and Analysis of Java Programs
Separation algebras	Separation algebras for C verification in Coq
sequential consistency	Store Buffer Reduction with MMUs
SMT solvers	Formalizing Semantics with an Automatic Program Verifier
software model checking	Model Checking Parameterized Timed Systems
Specifications	A logical analysis of framing for specifications with pure method calls
step-wise refinement	Efficient Refinement Checking in VCC
Store buffer reduction	Store Buffer Reduction with MMUs
stuttering bisimulations	Timed Refinements for Verification of Real-Time Object Code Programs
System description	The KeY Platform for Verification and Analysis of Java Programs
T
term rewriting	Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
testing	The KeY Platform for Verification and Analysis of Java Programs
theorem proving	The KeY Platform for Verification and Analysis of Java Programs
timed automata	Model Checking Parameterized Timed Systems
timed transition systems	Timed Refinements for Verification of Real-Time Object Code Programs
TLB	Store Buffer Reduction with MMUs
V
verification	Store Buffer Reduction with MMUs Formal Modeling and Verification of CloudProxy The KeY Platform for Verification and Analysis of Java Programs
Verification conditions	A Verification Condition Visualizer
verification of object code	Timed Refinements for Verification of Real-Time Object Code Programs
verified RTOS	Efficient Refinement Checking in VCC
Verified verifiers	Using Promela in a Fully Verified Executable LTL Model Checker (SHORT)
visualization	A Verification Condition Visualizer The KeY Platform for Verification and Analysis of Java Programs

Disclaimer | Powered by EasyChair Smart Program