Linked e-resources
Details
Table of Contents
Invited Contributions
Can Formal Methods Improve the Efficiency of Code Reviews.-Symbolic Computation and Automated Reasoning for Program Analysis
Program verification
On Type Checking Delta-Oriented Product Lines
Verifying a priority scheduler for an SCJ runtime environment
Why Just Boogie? Translating Between Intermediate Verification Languages
Probabilistic systems
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata
Probabilistic Formal Analysis of App Usage to Inform Redesign
Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC
Concurrency
Monitoring Multi-threaded Component-Based Systems
A Generalised Theory of Interface Automata, Component Compatibility and Error
On Implementing a Monitor-Oriented Programming Framework for Actor Systems
Towards a Thread-Local Proof Technique for Starvation Freedom
Reasoning about Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems
A Formal Model of the Safety-Critical Java Level 2 Paradigm
Safety and liveness
Deciding Monadic Second Order Logic over omega-words by Specialized Finite Automata
Property Preservation for Extension Patterns of State Transition Diagrams
Symbolic Reachability Analysis of B through ProB and LTSmin
Model learning
Enhancing Automata Learning by Log-Based Metrics
Refactoring of Legacy Software using Model Learning and Equivalence Checking: an Industrial Experience Report
On Robust Malware Classifiers by Verifying Unwanted Behaviours
SAT and SMT solving
Efficient Deadlock-Freedom Checking using Local Analysis and SAT Solving
SMT Solvers for Validation of B and Event-B models
Avoiding Medication Conflicts for Patients with Multimorbidities
Testing
Temporal Random Testing for Spark Streaming
Combining Static Analysis and Testing for Deadlock Detection
Fuzzing JavaScript Engine APIs
Theorem proving and constraint satisfaction
A Component-based Approach to Hybrid Systems Safety Verification
Verifying Pointer Programs using Separation Logic and Invariant Based Programming in Isabelle
A Constraint Satisfaction Method for Configuring Non-Local Service Interfaces
Case studies
Rule-based Consistency Checking of Railway Infrastructure Designs
Formal Verification of Safety PLC Based Control Software
Enabling Static Driver Verifier using Microsoft Azure.
Can Formal Methods Improve the Efficiency of Code Reviews.-Symbolic Computation and Automated Reasoning for Program Analysis
Program verification
On Type Checking Delta-Oriented Product Lines
Verifying a priority scheduler for an SCJ runtime environment
Why Just Boogie? Translating Between Intermediate Verification Languages
Probabilistic systems
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata
Probabilistic Formal Analysis of App Usage to Inform Redesign
Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC
Concurrency
Monitoring Multi-threaded Component-Based Systems
A Generalised Theory of Interface Automata, Component Compatibility and Error
On Implementing a Monitor-Oriented Programming Framework for Actor Systems
Towards a Thread-Local Proof Technique for Starvation Freedom
Reasoning about Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems
A Formal Model of the Safety-Critical Java Level 2 Paradigm
Safety and liveness
Deciding Monadic Second Order Logic over omega-words by Specialized Finite Automata
Property Preservation for Extension Patterns of State Transition Diagrams
Symbolic Reachability Analysis of B through ProB and LTSmin
Model learning
Enhancing Automata Learning by Log-Based Metrics
Refactoring of Legacy Software using Model Learning and Equivalence Checking: an Industrial Experience Report
On Robust Malware Classifiers by Verifying Unwanted Behaviours
SAT and SMT solving
Efficient Deadlock-Freedom Checking using Local Analysis and SAT Solving
SMT Solvers for Validation of B and Event-B models
Avoiding Medication Conflicts for Patients with Multimorbidities
Testing
Temporal Random Testing for Spark Streaming
Combining Static Analysis and Testing for Deadlock Detection
Fuzzing JavaScript Engine APIs
Theorem proving and constraint satisfaction
A Component-based Approach to Hybrid Systems Safety Verification
Verifying Pointer Programs using Separation Logic and Invariant Based Programming in Isabelle
A Constraint Satisfaction Method for Configuring Non-Local Service Interfaces
Case studies
Rule-based Consistency Checking of Railway Infrastructure Designs
Formal Verification of Safety PLC Based Control Software
Enabling Static Driver Verifier using Microsoft Azure.