top

  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.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.
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
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]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
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
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]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
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
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
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
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
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
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
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
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
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
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
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
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Model-Based Testing of Reactive Systems [[electronic resource] ] : Advanced Lectures / / edited by Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner
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
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Runtime Verification [[electronic resource] ] : 18th International Conference, RV 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings / / edited by Christian Colombo, Martin Leucker
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
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Runtime Verification : 18th International Conference, RV 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings / / edited by Christian Colombo, Martin Leucker
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
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Runtime verification : 8th international workshop, RV 2008, Budapest, Hungary, March 30, 2008 : selected papers / / Martin Leucker (editor)
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]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui