VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

A
aggregation	Programming Language Aggregation with Applications in Equivalence Checking
Algorithm	Synthesis of Algorithms on Sets Represented as Monotone Lists Symbolic Problem Solving With Bidirectional Executable Representations
Android	Automatic App Testing of LTL Properties
app	Automatic App Testing of LTL Properties
Automation of Mathematics	The Theorema Approach to Mathematics
B
Bidirectional	Symbolic Problem Solving With Bidirectional Executable Representations
C
classical first-order logic with inductive predicates	Building explicit induction schemas for cyclic induction reasoning
completeness	A Model Theory for R-calculus without Cut
confluence	Confluence of Pattern-Based Calculi with Finitary Matching
constraint solver	A hybrid path constraint solver combined with meta-heuristic search
constraint solving	Automated verification of security protocols and services
conversion algorithm	The Verification of Conversion Algorithms between Finite Automata
crawling	Automatic App Testing of LTL Properties
cyclic and structural induction	Building explicit induction schemas for cyclic induction reasoning
D
Design	Symbolic Problem Solving With Bidirectional Executable Representations
Dynamic Analysis	Source code profiling and classification for automated detection of logical errors
E
equivalence	Programming Language Aggregation with Applications in Equivalence Checking
Extraction	Synthesis of Algorithms on Sets Represented as Monotone Lists
F
Finitary matching	Confluence of Pattern-Based Calculi with Finitary Matching
finite automata	The Verification of Conversion Algorithms between Finite Automata
first-order logic	An Attempt to Formalize Popper's Logic of Scientific Discovery
formal methods	Programming Language Aggregation with Applications in Equivalence Checking
formal specification	Symbolic Problem Solving With Bidirectional Executable Representations
formal verification of OS	VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
fuzzy logic	Source code profiling and classification for automated detection of logical errors
I
Imperative Program	Symbolic Problem Solving With Bidirectional Executable Representations
induction reasoning	Building explicit induction schemas for cyclic induction reasoning
Input Vectors	Source code profiling and classification for automated detection of logical errors
insertion modeling	New predicate transformer for symbolic modeling
integrity of OS	VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
Invariants	Source code profiling and classification for automated detection of logical errors
Isabelle/HOL	VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
K
Knowledge	Symbolic Problem Solving With Bidirectional Executable Representations
L
Logic of Scientific Discovery	An Attempt to Formalize Popper's Logic of Scientific Discovery
Logical Errors	Source code profiling and classification for automated detection of logical errors
LTL	Automatic App Testing of LTL Properties
M
matching logic	Programming Language Aggregation with Applications in Equivalence Checking
maximal contraction	RCK: A Software Toolkit for R-calculus
meta-heuristic search	A hybrid path constraint solver combined with meta-heuristic search
micro-kernel OS	VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
mobile computing	Automatic App Testing of LTL Properties
model	A Model Theory for R-calculus without Cut
N
Noetherian induction	Building explicit induction schemas for cyclic induction reasoning
Nonlinear Real Arithmetic	A note on real quantifier elimination by virtual term substitution of unbounded degree
O
OS FSM model	VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
P
partial correctness	Programming Language Aggregation with Applications in Equivalence Checking
Pattern calculus	Confluence of Pattern-Based Calculi with Finitary Matching
predicate transformer	New predicate transformer for symbolic modeling
proof	Synthesis of Algorithms on Sets Represented as Monotone Lists
Q
quantifier elimination	A note on real quantifier elimination by virtual term substitution of unbounded degree
R
R-calculus	RCK: A Software Toolkit for R-calculus
real algebra	A note on real quantifier elimination by virtual term substitution of unbounded degree
Refutation	An Attempt to Formalize Popper's Logic of Scientific Discovery
revision calculus	An Attempt to Formalize Popper's Logic of Scientific Discovery A Model Theory for R-calculus without Cut
S
safety-critical real-time systems	Successfully Coping with Scalability of Symbolic Analysis in Timing Analysis
secure services	Automated verification of security protocols and services
security protocols	Automated verification of security protocols and services
semantics	Programming Language Aggregation with Applications in Equivalence Checking
sequent-based systems	Building explicit induction schemas for cyclic induction reasoning
Software Science	The Theorema Approach to Mathematics
software testing	Automatic App Testing of LTL Properties
software toolkit	RCK: A Software Toolkit for R-calculus
soundness	A Model Theory for R-calculus without Cut
Source code classification	Source code profiling and classification for automated detection of logical errors
Static Analysis	Source code profiling and classification for automated detection of logical errors
Symbolic analysis	Successfully Coping with Scalability of Symbolic Analysis in Timing Analysis
symbolic execution	A hybrid path constraint solver combined with meta-heuristic search
synthesis	Synthesis of Algorithms on Sets Represented as Monotone Lists
T
Theorema	The Theorema Approach to Mathematics
timing analysis	Successfully Coping with Scalability of Symbolic Analysis in Timing Analysis
V
validity	A Model Theory for R-calculus without Cut
verification	Programming Language Aggregation with Applications in Equivalence Checking Automated verification of security protocols and services The Verification of Conversion Algorithms between Finite Automata
verification of requirement specification	New predicate transformer for symbolic modeling
virtual term substitution	A note on real quantifier elimination by virtual term substitution of unbounded degree

Disclaimer | Powered by EasyChair Smart Program