Formal Methods: Foundations and Applications: 25th Brazilian Symposium, SBMF 2022, Virtual Event, December 6–9, 2022, Proceedings

Preface
Organization
Invited Talks
	Cooperative Verification
	Taming Monsters with Dragons: A Fractal Approach to Digital Twin Pipelines
	Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community
	Some Applications of Formal Methods
	Contents
Model Checking and Semantics
An Efficient Customized Clock Allocation Algorithm for a Class of Timed Automata
	1 Introduction
	2 Timed automata
	3 The Class TADS
	4 The Notion of Optimality
	5 Finding an Optimal Allocation of Clocks
		5.1 Liveness Analysis of Clocks
		5.2 Clock Allocation
		5.3 The Clock Allocation Algorithm
		5.4 Generating Clock Constraints and Clock Resets
	6 Related Work and Conclusions
	References
Formalization of Functional Block Diagrams Using HOL Theorem Proving
	1 Introduction
	2 Preliminaries
		2.1 Formal ET Modeling
		2.2 Formal ET Probabilistic Analysis
	3 Functional Block Diagrams
	4 FBD Formalization
		4.1 Formal FBD Modeling
		4.2 Formal FBD Probabilistic Analysis
	5 Conclusions
	References
Generation and Synthesis
A Sound Strategy to Compile General Recursion into Finite Depth Pattern Matching
	1 Introduction
	2 Basic Definitions
	3 Expansion and Transformation
		3.1 Unrolling
		3.2 Recursion Elimination
	4 Term Generation
		4.1 Soundness of Term Generation
	5 Quick-Checking Properties
	6 Related Work
	7 Conclusion
	References
Automatic Generation of Verified Concurrent Hardware Using VHDL
	1 Introduction
		1.1 Related Work
	2 Theoretical Background
		2.1 CSP
		2.2 VHDL
	3 CSP to VHDL Translation
		3.1 Translation Overview
		3.2 Restrictions
	4 Tool Support
	5 Case Study
	6 Conclusion
	References
Synthesis of Implementations for Divide-and-Conquer Specifications
	1 Introduction
	2 Preliminaries
	3 From Divide-and-Conquer Specifications to Their Implementations
		3.1 The Synthesis Rule
	4 Case Study: Deriving an Implementation of a Greedy Algorithm
		4.1 Weighted Matroids and Their Bases
		4.2 Establishing max-basisI as a Divide-and-Conquer Specification
		4.3 Implementations of Decomposition and Composition
	5 Related Work
	6 Conclusions and Outlook
	A The Three Auxiliary Lemmas
	References
Verification and Solvers
Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover
	1 Introduction
	2 Background
		2.1 Block Diagrams and MDD
		2.2 Running Example - Simple Actuator System (SAS)
		2.3 Formal Verification and CSP
		2.4 tock-CSP
		2.5 Roscoe and Dathi's Compositional Deadlock Analysis Theory
		2.6 CSP-Prover
	3 Mechanised Compositional Verification of Timed Process Networks
		3.1 Time-Stop Free Processes
		3.2 Time-Stop Free Process Networks
		3.3 Mechanisation in CSP-Prover
	4 From Simulink to tock-CSP
	5 Conclusion and Future Works
	References
Excommunication: Transforming -Calculus Specifications to Remove Internal Communication
	1 Introduction
	2 The -Calculus
	3 The Excommunication Algorithm
		3.1 Transformation Rules
	4 Example Application: A Leakage Analysis
		4.1 An Application of the Leakage Analysis
	5 Conclusion and Further Work
	References
Level-Up - From Bits to Words
	1 Introduction
	2 Background
		2.1 Verification Using Satisfiability Solvers
		2.2 Word-Level Verification
	3 Using Bit-Level Information on Word-Level
		3.1 Computing Bit-Level Information
		3.2 Bit-Level Information for the Example
		3.3 Integration Strategies
		3.4 Integration Strategies for Bit-Level Information
		3.5 Implementation and Tool Chain
	4 Evaluation Experiments
		4.1 Experimental Setup
		4.2 Experimental Results
	5 Related Work
	6 Conclusion and Outlook
	References
Author Index