Formal methods: foundations and applications : 25th Brazilian symposium, SBMF 2022, virtual event, December 6-9, 2022, proceedings / / Lucas Lima, Vince Molnár (editors)

• Pubblicazione: Cham, Switzerland : , : Springer, , [2022]; ©2022
• Descrizione fisica: 1 online resource (154 pages)
• Disciplina: 005.1
• Soggetto topico: Computer software - Development; Formal methods (Computer science)
• Persona (resp. second.): MolnárVince; LimaLucas
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Intro -- 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.
• Titolo autorizzato: Formal Methods: Foundations and Applications
• ISBN: 3-031-22476-0
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 996500061203316
• Lo trovi qui: Univ. di Salerno
• Serie: Lecture notes in computer science ; ; Volume 13768.