LEADER 05554nam 2200505 450 001 996500061203316 005 20230414181627.0 010 $a3-031-22476-0 035 $a(MiAaPQ)EBC7150675 035 $a(Au-PeEL)EBL7150675 035 $a(CKB)25510542000041 035 $a(OCoLC)1352973612 035 $a(PPN)266348890 035 $a(EXLCZ)9925510542000041 100 $a20230414d2022 uy 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 00$aFormal methods: foundations and applications $e25th Brazilian symposium, SBMF 2022, virtual event, December 6-9, 2022, proceedings /$fLucas Lima, Vince Molna?r (editors) 210 1$aCham, Switzerland :$cSpringer,$d[2022] 210 4$d©2022 215 $a1 online resource (154 pages) 225 1 $aLecture notes in computer science ;$vVolume 13768 311 08$aPrint version: Lima, Lucas Formal Methods: Foundations and Applications Cham : Springer International Publishing AG,c2023 9783031224751 320 $aIncludes bibliographical references and index. 327 $aIntro -- 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. 327 $a3 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. 327 $a6 Conclusion and Outlook -- References -- Author Index. 410 0$aLecture notes in computer science ;$vVolume 13768. 606 $aComputer software$xDevelopment$vCongresses 606 $aFormal methods (Computer science)$vCongresses 615 0$aComputer software$xDevelopment 615 0$aFormal methods (Computer science) 676 $a005.1 702 $aMolna?r$b Vince 702 $aLima$b Lucas 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996500061203316 996 $aFormal Methods: Foundations and Applications$9773789 997 $aUNISA