Linked e-resources
Details
Table of Contents
Invited Papers
Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems
Satisfiability Checking: Theory and Applications
Concurrency and Non-Interference
Automatic Derivation of Platform Noninterference Properties
Linearizability and Causality
Refinement-based verification of Communicating Unstructured Code
Guided Dynamic Symbolic Execution Using Subgraph Control-Flow Information (short paper)
Program Analysis
Correlating Structured Inputs and Outputs in Functional Specifications
Combining Predicate Abstraction with Fixpoint Approximations
Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis
Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block Diagrams
Model Checking
Program Generation using Simulated Annealing and Model Checking
LTL Parameter Synthesis of Parametric Timed Automata
Model checking simulation rules for linearizability
LTL Model Checking under Fairness in ProB (short paper)
Verification
Counterexamples from Proof Failures in SPARK
Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
SMT-based automatic proof of ASM model refinement
Coq Implementation of OO Verification Framework VeriJ (short paper)
Towards a Proof Framework for Information Systems with Weak Consistency (short paper)
Interaction and Adaptation
A Cognitive Framework based on Rewriting Logic for the Analysis of Interactive Systems
Incentive Stackelberg Mean-payoff Games
Stability-based Adaptation of Asynchronously Communicating Software
Compliance Checking in the Open Payments Ecosystem (short paper)
Development Methods
CoCoSpec: A mode aware contract language
Modularizing Crosscutting Concerns in Component-Based Systems
Tightening a Contract Refinement
BMotionWeb: A Tool for Rapid Creation of Formal Prototypes.
Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems
Satisfiability Checking: Theory and Applications
Concurrency and Non-Interference
Automatic Derivation of Platform Noninterference Properties
Linearizability and Causality
Refinement-based verification of Communicating Unstructured Code
Guided Dynamic Symbolic Execution Using Subgraph Control-Flow Information (short paper)
Program Analysis
Correlating Structured Inputs and Outputs in Functional Specifications
Combining Predicate Abstraction with Fixpoint Approximations
Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis
Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block Diagrams
Model Checking
Program Generation using Simulated Annealing and Model Checking
LTL Parameter Synthesis of Parametric Timed Automata
Model checking simulation rules for linearizability
LTL Model Checking under Fairness in ProB (short paper)
Verification
Counterexamples from Proof Failures in SPARK
Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
SMT-based automatic proof of ASM model refinement
Coq Implementation of OO Verification Framework VeriJ (short paper)
Towards a Proof Framework for Information Systems with Weak Consistency (short paper)
Interaction and Adaptation
A Cognitive Framework based on Rewriting Logic for the Analysis of Interactive Systems
Incentive Stackelberg Mean-payoff Games
Stability-based Adaptation of Asynchronously Communicating Software
Compliance Checking in the Open Payments Ecosystem (short paper)
Development Methods
CoCoSpec: A mode aware contract language
Modularizing Crosscutting Concerns in Component-Based Systems
Tightening a Contract Refinement
BMotionWeb: A Tool for Rapid Creation of Formal Prototypes.