ABZ2023: 9TH INTERNATIONAL CONFERENCE ON RIGOROUS STATE-BASED METHODS

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

A
abstract state machine	Behavioural Theory of Reflective Algorithms
abstract state machines	formal MVC: a pattern for the integration of ASM specifications in UI development Modeling the MVM-Adapt System by Compositional I/O Abstract State Machines
Abstraction	Validation by Abstraction and Refinement
actions formulas	Generating safe code to prevent or handle integer overflows inside Event-B actions formulas
adaptivity	Behavioural Theory of Reflective Algorithms
Air traffic control	Task Model Design and Analysis with Alloy
Alloy	Task Model Design and Analysis with Alloy Adding records to Alloy Crucible Tools for Test Generation and Advanced Animation of Alloy Models Teaching Alloy with Alloy4Fun
animation	Crucible Tools for Test Generation and Advanced Animation of Alloy Models
Arrival manager	Task Model Design and Analysis with Alloy
asm	Compositional Simulation of Abstract State Machines for Safety Critical Systems
ASMETA	Modeling the MVM-Adapt System by Compositional I/O Abstract State Machines
ASTD	TASTD a real-time extension for ASTD Modelling an Automotive Software System with TASTD
Autmoatic verification	VerCors & Alpinist: verification of optimised GPU programs
Automated Theorem Proving	Encoding TLA+ Proof Obligations Safely for SMT
Automatic theorem provers	Using Lambdapi to verify proof obligations of TLAPS generated by veriT
B
B and Z	{log}: Programming and Automated Proof in Set Theory (I) {log}: Programming and Automated Proof in Set Theory (II)
B formal model	Introducing Inductive Construction in B with the Theory Plugin
B method	Using B to program the CLEARSY Safety Platform Starter Kit For Education Rodin: two years of updates
B-Method	Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems
behavioural theory	Behavioural Theory of Reflective Algorithms
C
Camille	CamilleX 3.0
case study	Modelling an Automotive Software System with TASTD A Case-study for Incremental Validation
Classification	Classification and Semantics of Validation Tasks
CoCoSpec	Exploring a methodology for formal verification of safety-critical systems
Compositional model-based simulation	Modeling the MVM-Adapt System by Compositional I/O Abstract State Machines
Conclusion	Wrap Up
Constraint Solver	Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems
copy protection	Exploration of Reflective ASMs for Genetic Algorithms and Security
Cyclone	Verifying Event-B Hybrid Models using Cyclone
D
Deadlock-freeness	Standalone Event-B models analysis relying on the EB4EB meta-theory
Development	Validation-Driven Development
Discrete Event Systems modeling	Modeling the MVM-Adapt System by Compositional I/O Abstract State Machines
Domain-specific	Validation of Formal Models by Interactive Simulation
E
e-voring	Formal verification of electronic voting systems
EB4EB framework	Standalone Event-B models analysis relying on the EB4EB meta-theory
embedded systems	Using B to program the CLEARSY Safety Platform Starter Kit For Education
Event-B	A framework for formal verification and validation of railway systems Exploring a methodology for formal verification of safety-critical systems Modeling and Analysis of a Safety-critical Interactive System through VOs Verifying Event-B Hybrid Models using Cyclone Pattern-based Refinement Generation Through Domain Specific Languages Journal-First: Building Specifications in the Event-B Institution Designing Secure Systems using Hierarchical STPA and Event-B Standalone Event-B models analysis relying on the EB4EB meta-theory Validation by Abstraction and Refinement Rodin: two years of updates Proof automation for Event-B theories Constructing the Real Numbers using RODIN and EBRP’s plugin CamilleX 3.0 Formalisation of a Software Development Process A Rigorous Iterative Analysis Approach for Capturing the Safety Requirements of Self-Driving Vehicle Systems: Generating safe code to prevent or handle integer overflows inside Event-B actions formulas Intro to the IVOIRE project Classification and Semantics of Validation Tasks Formalizing and Validating the VO Approach
Event-B method	Modeling and Verifying an Arrival Manager using Event-B
F
Floating-Point Numbers	Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems
Formal design	Designing Secure Systems using Hierarchical STPA and Event-B
formal method	Modelling an Automotive Software System with TASTD Formal verification of electronic voting systems Using B to program the CLEARSY Safety Platform Starter Kit For Education
Formal Methods	A framework for formal verification and validation of railway systems Exploring a methodology for formal verification of safety-critical systems Validation of Formal Models by Interactive Simulation Validation by Abstraction and Refinement TASTD a real-time extension for ASTD
Formal specification	Adding records to Alloy
formula-program duality	{log}: Programming and Automated Proof in Set Theory (I) {log}: Programming and Automated Proof in Set Theory (II)
FRET	Exploring a methodology for formal verification of safety-critical systems
G
genetic algorithms	Exploration of Reflective ASMs for Genetic Algorithms and Security
H
HAMSTERS	Task Model Design and Analysis with Alloy
Haskell	Rodin-hs: A set of libraries and tools for handling Rodin files in Haskell
High-level requirements	Pattern-based Refinement Generation Through Domain Specific Languages
Hybrid Systems	Verifying Event-B Hybrid Models using Cyclone
I
incremental process	A Case-study for Incremental Validation
Inductive construction	Introducing Inductive Construction in B with the Theory Plugin
Institutions	Journal-First: Building Specifications in the Event-B Institution
Interactive	Validation of Formal Models by Interactive Simulation
Interactive system analysis	Task Model Design and Analysis with Alloy
Interactive Verification	Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems
Interoperability	Journal-First: Building Specifications in the Event-B Institution
Invariant weakness	Standalone Event-B models analysis relying on the EB4EB meta-theory
IVOIRE	Intro to the IVOIRE project Wrap Up
L
Lambdapi	Using Lambdapi to verify proof obligations of TLAPS generated by veriT
linguistic reflection	Behavioural Theory of Reflective Algorithms
M
Meta-Theory	Standalone Event-B models analysis relying on the EB4EB meta-theory
model checking	Adding records to Alloy Verifying temporal relational models with Pardinus
model finding	Verifying temporal relational models with Pardinus
model-view-controller	formal MVC: a pattern for the integration of ASM specifications in UI development
Modelchecking	Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems
modelling	Teaching Alloy with Alloy4Fun Validation-Driven Development
Modularisation	Journal-First: Building Specifications in the Event-B Institution
O
obligation	Formalizing and Validating the VO Approach
P
pattern for user interfaces	formal MVC: a pattern for the integration of ASM specifications in UI development
Pattern-based development	Pattern-based Refinement Generation Through Domain Specific Languages
ProB	Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems
Process	Formalisation of a Software Development Process
Programming language	{log}: Programming and Automated Proof in Set Theory (I) {log}: Programming and Automated Proof in Set Theory (II)
Proof	Proof automation for Event-B theories
Proof activity	Introducing Inductive Construction in B with the Theory Plugin
proof assistants	Using Lambdapi to verify proof obligations of TLAPS generated by veriT
proof verification	Using Lambdapi to verify proof obligations of TLAPS generated by veriT
Proofs	Constructing the Real Numbers using RODIN and EBRP’s plugin
R
Railway systems	A framework for formal verification and validation of railway systems
Reachability	Standalone Event-B models analysis relying on the EB4EB meta-theory
Real Numbers	Constructing the Real Numbers using RODIN and EBRP’s plugin
real-time model	Modelling an Automotive Software System with TASTD
real-time models	TASTD a real-time extension for ASTD
recombinative simulated annealing	Exploration of Reflective ASMs for Genetic Algorithms and Security
Refactoring	Exploring a methodology for formal verification of safety-critical systems
Refinement	Modeling and Verifying an Arrival Manager using Event-B Modeling and Analysis of a Safety-critical Interactive System through VOs Validation by Abstraction and Refinement Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems
Refinement and Proof	Standalone Event-B models analysis relying on the EB4EB meta-theory
Reflection	Standalone Event-B models analysis relying on the EB4EB meta-theory
reflective Abstract State Machines	Exploration of Reflective ASMs for Genetic Algorithms and Security
relational logic	Verifying temporal relational models with Pardinus
Requirements	Validation of Formal Models by Interactive Simulation Designing Secure Systems using Hierarchical STPA and Event-B
Rodin	Introducing Inductive Construction in B with the Theory Plugin Rodin: two years of updates Constructing the Real Numbers using RODIN and EBRP’s plugin Rodin-hs: A set of libraries and tools for handling Rodin files in Haskell CamilleX 3.0 Formalisation of a Software Development Process A Rigorous Iterative Analysis Approach for Capturing the Safety Requirements of Self-Driving Vehicle Systems: Intro to the IVOIRE project
S
safe code	Generating safe code to prevent or handle integer overflows inside Event-B actions formulas
safety	Designing Secure Systems using Hierarchical STPA and Event-B Compositional Simulation of Abstract State Machines for Safety Critical Systems
safety platform	Using B to program the CLEARSY Safety Platform Starter Kit For Education
satisfiability	{log}: Programming and Automated Proof in Set Theory (I) {log}: Programming and Automated Proof in Set Theory (II)
Security	Designing Secure Systems using Hierarchical STPA and Event-B
security protocols	Formal verification of electronic voting systems
self-driving syst(ems	A Rigorous Iterative Analysis Approach for Capturing the Safety Requirements of Self-Driving Vehicle Systems:
Semantics	Journal-First: Building Specifications in the Event-B Institution
Simulation	Modeling and Analysis of a Safety-critical Interactive System through VOs Validation of Formal Models by Interactive Simulation Compositional Simulation of Abstract State Machines for Safety Critical Systems
SMT	Encoding TLA+ Proof Obligations Safely for SMT
Software Verification	Exploring a methodology for formal verification of safety-critical systems
Standard conformance	A framework for formal verification and validation of railway systems
State-Based Concurrent Systems	Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems
Step-wise refinement	Pattern-based Refinement Generation Through Domain Specific Languages
STPA	Designing Secure Systems using Hierarchical STPA and Event-B
System modeling	A framework for formal verification and validation of railway systems Modeling and Verifying an Arrival Manager using Event-B
T
Task models	Task Model Design and Analysis with Alloy
TASTD	TASTD a real-time extension for ASTD Modelling an Automotive Software System with TASTD
temporal logic	Verifying temporal relational models with Pardinus
test generation	Crucible Tools for Test Generation and Advanced Animation of Alloy Models
Theories	Proof automation for Event-B theories Constructing the Real Numbers using RODIN and EBRP’s plugin
Theory Plugin	Introducing Inductive Construction in B with the Theory Plugin
Thread-Local Proof Obligations	Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems
TLA+	Encoding TLA+ Proof Obligations Safely for SMT
TLAPS	Using Lambdapi to verify proof obligations of TLAPS generated by veriT Encoding TLA+ Proof Obligations Safely for SMT
Tool feedback	Introducing Inductive Construction in B with the Theory Plugin
Tools	Rodin-hs: A set of libraries and tools for handling Rodin files in Haskell
V
Validation	Validation of Formal Models by Interactive Simulation Validation by Abstraction and Refinement VerCors & Alpinist: verification of optimised GPU programs Teaching Alloy with Alloy4Fun Intro to the IVOIRE project Classification and Semantics of Validation Tasks Formalizing and Validating the VO Approach Validation-Driven Development A Case-study for Incremental Validation
Validation Obligations	Modeling and Analysis of a Safety-critical Interactive System through VOs Validation by Abstraction and Refinement
verification	Modeling and Verifying an Arrival Manager using Event-B Verifying Event-B Hybrid Models using Cyclone VerCors & Alpinist: verification of optimised GPU programs {log}: Programming and Automated Proof in Set Theory (I) Teaching Alloy with Alloy4Fun {log}: Programming and Automated Proof in Set Theory (II)
veriT	Using Lambdapi to verify proof obligations of TLAPS generated by veriT
Visualization	Modeling and Analysis of a Safety-critical Interactive System through VOs Validation of Formal Models by Interactive Simulation
W
Workshop	Wrap Up

Disclaimer | Powered by EasyChair Smart Program