Formal methods : 25th international symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, proceedings / / edited by Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker |
Edizione | [1st ed. 2023.] |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2023] |
Descrizione fisica | 1 online resource (661 pages) |
Disciplina | 004.0151 |
Collana | Lecture Notes in Computer Science |
Soggetto topico | Formal methods (Computer science) |
ISBN | 3-031-27481-4 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Keynotes -- Symbolic Computation in Automated Program Reasoning -- The next big thing: from embedded systems to embodied actors -- Intelligent and Dependable Decision-Making Under Uncertainty -- A Coq formalization of Lebesgue Induction Principle and Tonelli’s Theorem -- SAT/SMT -- Railway Scheduling Using Boolean Satisfiability Modulo Simulations -- SMT Sampling via Model-Guided Approximation -- Efficient SMT-based Network Fault Tolerance Verification -- Verification I -- Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems -- Can we Communicate? Using Dynamic Logic to Verify Team Automata -- The ScalaFix equation solver -- HHLPy: Practical Verification of Hybrid Systems using Hoare Logic -- Quantitative Verification -- symQV: Automated Symbolic Verification of Quantum Programs -- PFL: a Probabilistic Logic for Fault Trees -- Energy Buechi Problems -- QMaude: quantitative specification and verification in rewriting logic -- Concurrency and Memory Models -- Minimisation of Spatial Models using Branching Bisimilarity -- Reasoning about Promises in Weak Memory Models with Event Structures -- A fine-grained semantics for arrays and pointers under weak memory models -- VeyMont: Parallelising Verified Programs instead of Verifying Parallel Programs -- Verification 2 -- Verifying At the Level of Java Bytecode -- Abstract Alloy Instances -- Monitoring the Internet Computer -- Word Equations in Synergy with Regular Constraints -- Formal Methods in AI -- Verifying Feedforward Neural Networks for Classification in Isabelle/HOL -- SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets -- The Octatope Abstract Domain for Verification of Neural Networks -- Program Semantics and Verification Technique for AI-centred Programs -- Safety and Reliability -- Tableaux for Realizability of Safety Specifications -- A Decision Diagram Operation for Reachability -- Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement -- A Runtime Environment for Contract Automata -- Industry Day -- Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny -- Shifting Left for Early Detection of Machine-Learning Bugs -- A Systematic Approach to Automotive Security -- Specification-Guided Critical Scenario Identification for Automated Driving -- Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks -- Backdoor Mitigation in Deep Neural Networks via Strategic Retraining -- veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System. |
Record Nr. | UNINA-9910678257703321 |
Cham, Switzerland : , : Springer, , [2023] | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Formal methods : 25th international symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, proceedings / / edited by Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker |
Edizione | [1st ed. 2023.] |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2023] |
Descrizione fisica | 1 online resource (661 pages) |
Disciplina | 004.0151 |
Collana | Lecture Notes in Computer Science |
Soggetto topico | Formal methods (Computer science) |
ISBN | 3-031-27481-4 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Keynotes -- Symbolic Computation in Automated Program Reasoning -- The next big thing: from embedded systems to embodied actors -- Intelligent and Dependable Decision-Making Under Uncertainty -- A Coq formalization of Lebesgue Induction Principle and Tonelli’s Theorem -- SAT/SMT -- Railway Scheduling Using Boolean Satisfiability Modulo Simulations -- SMT Sampling via Model-Guided Approximation -- Efficient SMT-based Network Fault Tolerance Verification -- Verification I -- Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems -- Can we Communicate? Using Dynamic Logic to Verify Team Automata -- The ScalaFix equation solver -- HHLPy: Practical Verification of Hybrid Systems using Hoare Logic -- Quantitative Verification -- symQV: Automated Symbolic Verification of Quantum Programs -- PFL: a Probabilistic Logic for Fault Trees -- Energy Buechi Problems -- QMaude: quantitative specification and verification in rewriting logic -- Concurrency and Memory Models -- Minimisation of Spatial Models using Branching Bisimilarity -- Reasoning about Promises in Weak Memory Models with Event Structures -- A fine-grained semantics for arrays and pointers under weak memory models -- VeyMont: Parallelising Verified Programs instead of Verifying Parallel Programs -- Verification 2 -- Verifying At the Level of Java Bytecode -- Abstract Alloy Instances -- Monitoring the Internet Computer -- Word Equations in Synergy with Regular Constraints -- Formal Methods in AI -- Verifying Feedforward Neural Networks for Classification in Isabelle/HOL -- SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets -- The Octatope Abstract Domain for Verification of Neural Networks -- Program Semantics and Verification Technique for AI-centred Programs -- Safety and Reliability -- Tableaux for Realizability of Safety Specifications -- A Decision Diagram Operation for Reachability -- Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement -- A Runtime Environment for Contract Automata -- Industry Day -- Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny -- Shifting Left for Early Detection of Machine-Learning Bugs -- A Systematic Approach to Automotive Security -- Specification-Guided Critical Scenario Identification for Automated Driving -- Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks -- Backdoor Mitigation in Deep Neural Networks via Strategic Retraining -- veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System. |
Record Nr. | UNISA-996517755403316 |
Cham, Switzerland : , : Springer, , [2023] | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods in Outer Space [[electronic resource] ] : Essays Dedicated to Klaus Havelund on the Occasion of His 65th Birthday / / edited by Ezio Bartocci, Yliès Falcone, Martin Leucker |
Autore | Bartocci Ezio (Computer scientist) |
Edizione | [1st ed. 2021.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
Descrizione fisica | 1 online resource (197 pages) |
Disciplina | 001.642 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computer science
Software engineering Artificial intelligence Computer engineering Computer networks Theory of Computation Software Engineering Artificial Intelligence Computer Engineering and Networks |
ISBN | 3-030-87348-X |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | The K Vision for the Future of Programming Language Design and Analysis -- Refining the Safety-Liveness Classification of Temporal Properties According to Realizability -- Domain Analysis & Description – Sorts, Types, Intents -- Dynamic interval analysis by abstract interpretation -- Runtime Verification: Passing on the Baton -- Hardware-Assisted Online Data Race Detection -- Comparing two methods for checking runtime properties -- Confidence Monitoring and Composition for Dynamic Assurance of Learning-Enabled Autonomous Systems -- Collision-Free 3D Flocking Using the Distributed Simplex Architecture -- A Context-Free Symbiosis of Runtime Verification & Automata Learning -- Reverse Engineering through Automata Learning. |
Record Nr. | UNISA-996464382903316 |
Bartocci Ezio (Computer scientist)
![]() |
||
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods in Outer Space : Essays Dedicated to Klaus Havelund on the Occasion of His 65th Birthday / / edited by Ezio Bartocci, Yliès Falcone, Martin Leucker |
Autore | Bartocci Ezio (Computer scientist) |
Edizione | [1st ed. 2021.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
Descrizione fisica | 1 online resource (197 pages) |
Disciplina | 001.642 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computer science
Software engineering Artificial intelligence Computer engineering Computer networks Theory of Computation Software Engineering Artificial Intelligence Computer Engineering and Networks |
ISBN | 3-030-87348-X |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | The K Vision for the Future of Programming Language Design and Analysis -- Refining the Safety-Liveness Classification of Temporal Properties According to Realizability -- Domain Analysis & Description – Sorts, Types, Intents -- Dynamic interval analysis by abstract interpretation -- Runtime Verification: Passing on the Baton -- Hardware-Assisted Online Data Race Detection -- Comparing two methods for checking runtime properties -- Confidence Monitoring and Composition for Dynamic Assurance of Learning-Enabled Autonomous Systems -- Collision-Free 3D Flocking Using the Distributed Simplex Architecture -- A Context-Free Symbiosis of Runtime Verification & Automata Learning -- Reverse Engineering through Automata Learning. |
Record Nr. | UNINA-9910506380803321 |
Bartocci Ezio (Computer scientist)
![]() |
||
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Formal Methods: Applications and Technology [[electronic resource] ] : 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected / / edited by Lubos Brim, Boudewijn Haverkort, Martin Leucker, Jaco van de Pol |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (371 p.) |
Disciplina | 004.0151 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computers
Software engineering Computer logic Programming languages (Electronic computers) Special purpose computers Theory of Computation Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Special Purpose and Application-Based Systems |
ISBN |
1-280-93577-4
9786610935772 3-540-70952-5 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Contributions -- Challenges for Formal Verification in Industrial Setting -- Distributed Verification: Exploring the Power of Raw Computing Power -- FMICS -- An Easy-to-Use, Efficient Tool-Chain to Analyze the Availability of Telecommunication Equipment -- ”To Store or Not To Store” Reloaded: Reclaiming Memory on Demand -- Discovering Symmetries -- On Combining Partial Order Reduction with Fairness Assumptions -- Test Coverage for Loose Timing Annotations -- Model-Based Testing of a WAP Gateway: An Industrial Case-Study -- Heuristics for ioco-Based Test-Based Modelling -- Verifying VHDL Designs with Multiple Clocks in SMV -- Verified Design of an Automated Parking Garage -- Evaluating Quality of Service for Service Level Agreements -- Simulation-Based Performance Analysis of a Medical Image-Processing Architecture -- Blasting Linux Code -- A Finite State Modeling of AFDX Frame Management Using Spin -- UML 2.0 State Machines: Complete Formal Semantics Via core state machine -- Automated Incremental Synthesis of Timed Automata -- SAT-Based Verification of LTL Formulas -- jmle: A Tool for Executing JML Specifications Via Constraint Programming -- Goanna—A Static Model Checker -- PDMC -- Parallel SAT Solving in Bounded Model Checking -- Parallel Algorithms for Finding SCCs in Implicitly Given Graphs -- Can Saturation Be Parallelised? -- Distributed Colored Petri Net Model-Checking with Cyclades. |
Record Nr. | UNISA-996466247603316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods: Applications and Technology : 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected / / edited by Lubos Brim, Boudewijn Haverkort, Martin Leucker, Jaco van de Pol |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (371 p.) |
Disciplina | 004.0151 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computers
Software engineering Computer logic Programming languages (Electronic computers) Special purpose computers Theory of Computation Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Special Purpose and Application-Based Systems |
ISBN |
1-280-93577-4
9786610935772 3-540-70952-5 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Contributions -- Challenges for Formal Verification in Industrial Setting -- Distributed Verification: Exploring the Power of Raw Computing Power -- FMICS -- An Easy-to-Use, Efficient Tool-Chain to Analyze the Availability of Telecommunication Equipment -- ”To Store or Not To Store” Reloaded: Reclaiming Memory on Demand -- Discovering Symmetries -- On Combining Partial Order Reduction with Fairness Assumptions -- Test Coverage for Loose Timing Annotations -- Model-Based Testing of a WAP Gateway: An Industrial Case-Study -- Heuristics for ioco-Based Test-Based Modelling -- Verifying VHDL Designs with Multiple Clocks in SMV -- Verified Design of an Automated Parking Garage -- Evaluating Quality of Service for Service Level Agreements -- Simulation-Based Performance Analysis of a Medical Image-Processing Architecture -- Blasting Linux Code -- A Finite State Modeling of AFDX Frame Management Using Spin -- UML 2.0 State Machines: Complete Formal Semantics Via core state machine -- Automated Incremental Synthesis of Timed Automata -- SAT-Based Verification of LTL Formulas -- jmle: A Tool for Executing JML Specifications Via Constraint Programming -- Goanna—A Static Model Checker -- PDMC -- Parallel SAT Solving in Bounded Model Checking -- Parallel Algorithms for Finding SCCs in Implicitly Given Graphs -- Can Saturation Be Parallelised? -- Distributed Colored Petri Net Model-Checking with Cyclades. |
Record Nr. | UNINA-9910483608403321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Model-Based Testing of Reactive Systems [[electronic resource] ] : Advanced Lectures / / edited by Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
Descrizione fisica | 1 online resource (VIII, 664 p.) |
Disciplina | 005.1/4 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Testing of Finite State Machines -- I. Testing of Finite State Machines -- 1 Homing and Synchronizing Sequences -- 2 State Identification -- 3 State Verification -- 4 Conformance Testing -- II. Testing of Labeled Transition Systems -- Testing of Labeled Transition Systems -- 5 Preorder Relations -- 6 Test Generation Algorithms Based on Preorder Relations -- 7 I/O-automata Based Testing -- 8 Test Derivation from Timed Automata -- 9 Testing Theory for Probabilistic Systems -- III. Model-Based Test Case Generation -- Model-Based Test Case Generation -- 10 Methodological Issues in Model-Based Testing -- 11 Evaluating Coverage Based Testing -- 12 Technology of Test-Case Generation -- 13 Real-Time and Hybrid Systems Testing -- IV. Tools and Case Studies -- Tools and Case Studies -- 14 Tools for Test Case Generation -- 15 Case Studies -- V. Standardized Test Notation and Execution Architecture -- Standardized Test Notation and Execution Architecture -- 16 TTCN-3 -- 17 UML 2.0 Testing Profile -- VI. Beyond Testing -- Beyond Testing -- 18 Run-Time Verification -- 19 Model Checking -- VII. Appendices -- Appendices -- 20 Model-Based Testing – A Glossary -- 21 Finite State Machines -- 22 Labelled Transition Systems. |
Record Nr. | UNISA-996466123103316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Runtime Verification [[electronic resource] ] : 18th International Conference, RV 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings / / edited by Christian Colombo, Martin Leucker |
Edizione | [1st ed. 2018.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
Descrizione fisica | 1 online resource (XI, 470 p. 113 illus., 42 illus. in color.) |
Disciplina | 005.14 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Compilers (Computer programs) Electronic digital computers—Evaluation Computer science Computers Professions Machine theory Software Engineering Compilers and Interpreters System Performance and Evaluation Computer Science Logic and Foundations of Programming The Computing Profession Formal Languages and Automata Theory |
ISBN | 3-030-03769-X |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Tutorial Papers -- Regular Papers -- Short Papers -- Tool Papers. |
Record Nr. | UNISA-996466290203316 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Runtime Verification : 18th International Conference, RV 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings / / edited by Christian Colombo, Martin Leucker |
Edizione | [1st ed. 2018.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
Descrizione fisica | 1 online resource (XI, 470 p. 113 illus., 42 illus. in color.) |
Disciplina | 005.14 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Compilers (Computer programs) Electronic digital computers—Evaluation Computer science Computers Professions Machine theory Software Engineering Compilers and Interpreters System Performance and Evaluation Computer Science Logic and Foundations of Programming The Computing Profession Formal Languages and Automata Theory |
ISBN | 3-030-03769-X |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Tutorial Papers -- Regular Papers -- Short Papers -- Tool Papers. |
Record Nr. | UNINA-9910349393203321 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Runtime verification : 8th international workshop, RV 2008, Budapest, Hungary, March 30, 2008 : selected papers / / Martin Leucker (editor) |
Edizione | [1st ed. 2008.] |
Pubbl/distr/stampa | Berlin ; ; Heidelberg ; ; New York : , : Springer, , [2008] |
Descrizione fisica | 1 online resource (VII, 189 p.) |
Disciplina | 004.0151 |
Collana | Lecture notes in computer science |
Soggetto topico | Formal methods (Computer science) |
ISBN | 3-540-89247-8 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | A Smell of Orchids -- Runtime Certification -- Model-Based Run-Time Checking of Security Permissions Using Guarded Objects -- Synthesizing Monitors for Safety Properties: This Time with Calls and Returns -- Forays into Sequential Composition and Concatenation in Eagle -- Checking Traces for Regulatory Conformance -- Deadlocks: From Exhibiting to Healing -- A Scalable, Sound, Eventually-Complete Algorithm for Deadlock Immunity -- Property Patterns for Runtime Monitoring of Web Service Conversations -- Runtime Monitoring of Object Invariants with Guarantee -- A Lightweight Container Architecture for Runtime Verification. |
Record Nr. | UNISA-996466242003316 |
Berlin ; ; Heidelberg ; ; New York : , : Springer, , [2008] | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|