Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Formal methods: foundations and applications : 25th Brazilian symposium, SBMF 2022, virtual event, December 6-9, 2022, proceedings / / Lucas Lima, Vince Molnár (editors)
| Formal methods: foundations and applications : 25th Brazilian symposium, SBMF 2022, virtual event, December 6-9, 2022, proceedings / / Lucas Lima, Vince Molnár (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (154 pages) |
| Disciplina | 005.1 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer software - Development
Formal methods (Computer science) |
| ISBN | 3-031-22476-0 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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. |
| Record Nr. | UNINA-9910633930503321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods: foundations and applications : 25th Brazilian symposium, SBMF 2022, virtual event, December 6-9, 2022, proceedings / / Lucas Lima, Vince Molnár (editors)
| Formal methods: foundations and applications : 25th Brazilian symposium, SBMF 2022, virtual event, December 6-9, 2022, proceedings / / Lucas Lima, Vince Molnár (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (154 pages) |
| Disciplina | 005.1 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer software - Development
Formal methods (Computer science) |
| ISBN | 3-031-22476-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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. |
| Record Nr. | UNISA-996500061203316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||