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 : 24th International Symposium, FM 2021, Virtual event, November 20-26, 2021, Proceedings / / Marieke Huisman, Corina Păsăreanu, Naijun Zhan (editors)
| Formal methods : 24th International Symposium, FM 2021, Virtual event, November 20-26, 2021, Proceedings / / Marieke Huisman, Corina Păsăreanu, Naijun Zhan (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (801 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-030-90870-4 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910508438803321 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods : 24th International Symposium, FM 2021, Virtual event, November 20-26, 2021, Proceedings / / Marieke Huisman, Corina Păsăreanu, Naijun Zhan (editors)
| Formal methods : 24th International Symposium, FM 2021, Virtual event, November 20-26, 2021, Proceedings / / Marieke Huisman, Corina Păsăreanu, Naijun Zhan (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (801 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-030-90870-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996464527203316 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering / / Gary T. Leavens, Alessandro Garcia, Corina S. Păsăreanu ; Association for Computing Machinery-Digital Library, contributor
| Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering / / Gary T. Leavens, Alessandro Garcia, Corina S. Păsăreanu ; Association for Computing Machinery-Digital Library, contributor |
| Autore | Leavens Gary T. |
| Pubbl/distr/stampa | New York, NY, USA : , : ACM, , 2018 |
| Descrizione fisica | 1 online resource |
| Disciplina | 005.1 |
| Collana | ACM Conferences |
| Soggetto topico | Software engineering |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910375699603321 |
Leavens Gary T.
|
||
| New York, NY, USA : , : ACM, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis / / Sarfraz Khurshid, Corina S. Păsăreanu, editors
| Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis / / Sarfraz Khurshid, Corina S. Păsăreanu, editors |
| Pubbl/distr/stampa | New York, NY : , : Association for Computing Machinery, , 2020 |
| Descrizione fisica | 1 online resource (591 pages) : illustrations |
| Disciplina | 005.30287 |
| Collana | ACM international conference proceedings series |
| Soggetto topico |
Computer software - Evaluation
Computer software - Testing |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910412068903321 |
| New York, NY : , : Association for Computing Machinery, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Software Engineering and Formal Methods [[electronic resource] ] : 19th International Conference, SEFM 2021, Virtual Event, December 6–10, 2021, Proceedings / / edited by Radu Calinescu, Corina S. Păsăreanu
| Software Engineering and Formal Methods [[electronic resource] ] : 19th International Conference, SEFM 2021, Virtual Event, December 6–10, 2021, Proceedings / / edited by Radu Calinescu, Corina S. Păsăreanu |
| Edizione | [1st ed. 2021.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
| Descrizione fisica | 1 online resource (524 pages) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Artificial intelligence Computer science Software Engineering Artificial Intelligence Theory of Computation |
| ISBN | 3-030-92124-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- RoboWorld: Where Can My Robot Work? -- Validating Safety Arguments with Lean -- Run-time Analysis and Testing -- Runtime Enforcement with Reordering, Healing, and Suppression -- Monitoring First-Order Interval Logic -- Exhaustive Property Oriented Model-based Testing With Symbolic Finite State Machines -- nfer - A Tool for Event Stream Abstraction -- Mining Shape Expressions with ShapeIt -- Security and Privacy -- Refining Privacy-Aware Data Flow Diagrams -- Hybrid Information Flow Control for Low-level Code -- Upper Bound Computation of Information Leakages for Unbounded Recursion -- On the Security and Safety of AbU Systems -- Parallel Composition/CSP and Probabilistic Reasoning -- Parallelized sequential composition and hardware weak memory models -- Checking Opacity and Durable Opacity with FDR -- Translation of CCS into CSP, Correct up toStrong Bisimulation -- Probabilistic BDI Agents: Actions, Plans, and Intentions -- A Debugger for Probabilistic Programs -- Verification and Synthesis -- Verification of Programs with Exceptions through Operator-Precedence Automata -- Counterexample Classification -- Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines -- Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL synthesis -- TACoS: A Tool for MTL Controller Synthesis -- Emerging Domains -- Lightweight Nontermination Inference with CHCs -- A Denotational Semantics of Solidity in Isabelle/HOL -- Configuration Space Exploration for Digital Printing Systems -- Bit-precise Verification of Discontinuity Errors Under Fixed-point Arithmetic -- Machine Learning and Cyber-Physical Systems -- OSIP: Tightened Bound Propagation for the Verification of ReLU Neural Networks -- Active Model Learning of Stochastic Reactive Systems -- Mixed-Neighborhood, Multi-Speed Cellular Automata for Safety-Aware Pedestrian Prediction. |
| Record Nr. | UNISA-996464508203316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Software Engineering and Formal Methods : 19th International Conference, SEFM 2021, Virtual Event, December 6–10, 2021, Proceedings / / edited by Radu Calinescu, Corina S. Păsăreanu
| Software Engineering and Formal Methods : 19th International Conference, SEFM 2021, Virtual Event, December 6–10, 2021, Proceedings / / edited by Radu Calinescu, Corina S. Păsăreanu |
| Edizione | [1st ed. 2021.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
| Descrizione fisica | 1 online resource (524 pages) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Artificial intelligence Computer science Software Engineering Artificial Intelligence Theory of Computation |
| ISBN | 3-030-92124-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- RoboWorld: Where Can My Robot Work? -- Validating Safety Arguments with Lean -- Run-time Analysis and Testing -- Runtime Enforcement with Reordering, Healing, and Suppression -- Monitoring First-Order Interval Logic -- Exhaustive Property Oriented Model-based Testing With Symbolic Finite State Machines -- nfer - A Tool for Event Stream Abstraction -- Mining Shape Expressions with ShapeIt -- Security and Privacy -- Refining Privacy-Aware Data Flow Diagrams -- Hybrid Information Flow Control for Low-level Code -- Upper Bound Computation of Information Leakages for Unbounded Recursion -- On the Security and Safety of AbU Systems -- Parallel Composition/CSP and Probabilistic Reasoning -- Parallelized sequential composition and hardware weak memory models -- Checking Opacity and Durable Opacity with FDR -- Translation of CCS into CSP, Correct up toStrong Bisimulation -- Probabilistic BDI Agents: Actions, Plans, and Intentions -- A Debugger for Probabilistic Programs -- Verification and Synthesis -- Verification of Programs with Exceptions through Operator-Precedence Automata -- Counterexample Classification -- Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines -- Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL synthesis -- TACoS: A Tool for MTL Controller Synthesis -- Emerging Domains -- Lightweight Nontermination Inference with CHCs -- A Denotational Semantics of Solidity in Isabelle/HOL -- Configuration Space Exploration for Digital Printing Systems -- Bit-precise Verification of Discontinuity Errors Under Fixed-point Arithmetic -- Machine Learning and Cyber-Physical Systems -- OSIP: Tightened Bound Propagation for the Verification of ReLU Neural Networks -- Active Model Learning of Stochastic Reactive Systems -- Mixed-Neighborhood, Multi-Speed Cellular Automata for Safety-Aware Pedestrian Prediction. |
| Record Nr. | UNINA-9910512185103321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Theoretical aspects of computing - ICTAC 2022 : 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, proceedings / / Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu
| Theoretical aspects of computing - ICTAC 2022 : 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, proceedings / / Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu |
| Autore | Seidl Helmut |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer International Publishing, , [2022] |
| Descrizione fisica | 1 online resource (494 pages) |
| Disciplina | 004 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer science
Computer science - Social aspects |
| ISBN | 3-031-17715-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- On Safety, Assurance and Reliability: A Software Engineering Perspective (Abstract of Invited Talk) -- Contents -- VeriMon: A Formally Verified Monitoring Tool -- 1 Introduction -- 2 Evolution -- 3 Future Directions -- 4 Discussion -- References -- Generalized Test Tables: A Domain-Specific Specification Language for Automated Production Systems -- 1 Introduction -- 2 The Domain of Automated Production Systems -- 3 Generalized Test Tables -- 4 Relational Test Tables -- 5 Conclusion -- References -- Reachability Games and Parity Games -- 1 Introduction -- 2 Games on Graphs -- 3 Reachability Games and Attractors -- 4 Optimal Strategies for Reachability Games -- 5 Parity Games -- 6 Zielonka's Algorithm for Parity Games -- 7 Lehtinen's Algorithm for Parity Games -- 8 Conclusion -- References -- Human-Cyber-Physical Automata and Their Synthesis -- 1 The Basic Model of HCPA -- 2 Synthesis of HCPS -- 3 Concluding Remarks -- References -- A PO Characterisation of Reconfiguration -- 1 Introduction -- 2 Labelled Partial Order Computations in a Nutshell -- 3 Preliminaries -- 3.1 Partial Orders and Labeled Partial Orders -- 3.2 Channelled Transition Systems (CTS) -- 3.3 Petri Nets with Inhibitor Arcs (PTI-nets) -- 4 LPO Semantics -- 4.1 Channelled Transition Systems (CTS) -- 4.2 Petri Nets with Inhibitor Arcs (PTI-nets) -- 5 Partial Order with Glue -- 5.1 Glue Computations for CTSs -- 5.2 Glue Computations for PTI-nets -- 6 Separating Choice and Forced Interleaving -- 6.1 Choice vs Reconfiguration-Forced Interleaving in CTSs -- 6.2 Choice vs Interleaving in PTI-nets -- 7 Concluding Remarks -- References -- Structural Rules and Algebraic Properties of Intersection Types -- 1 Introduction -- 2 Type Systems -- 3 Term Expansion -- 4 Conclusions -- References -- Quantitative Weak Linearisation -- 1 Introduction.
2 Terms and Reductions -- 3 Types -- 4 Weak-Linearisation for Strongly Normalising Terms -- 5 A Characterisation of Weak-Linear Terms -- 6 Related Works and Discussions -- 7 Conclusions and Future Work -- References -- On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems -- 1 Introduction -- 1.1 Related Work -- 2 Motivating Example Involving Drones -- 3 Timed Multiset Rewriting -- 4 Timed MSR for Resilient Systems -- 5 Verification Problems -- 6 Computational Complexity Results -- 7 Conclusions -- References -- Spatial and Timing Properties in Highway Traffic -- 1 Introduction -- 2 Preliminaries -- 2.1 Abstract Model of Motorway Traffic -- 2.2 Evolution of a Traffic Snapshot -- 2.3 MLSL with Scopes -- 2.4 State-Clock Logic -- 2.5 First-Order Theory of Real-Closed Fields -- 3 Timed MLSL -- 4 Semi-decision Procedure for TMLSL -- 5 Conclusion -- References -- Denotational and Algebraic Semantics for the CaIT Calculus -- 1 Introduction -- 2 The CaIT Calculus -- 2.1 Syntax -- 2.2 Guided Choice -- 3 Denotational Semantics -- 3.1 Semantic Model -- 3.2 Healthiness Conditions -- 3.3 Denotational Semantics of Basic Commands -- 3.4 Denotational Semantics of Guarded Choice -- 3.5 Parallel Composition -- 3.6 Channel Restriction -- 4 Algebraic Semantics -- 4.1 Algebraic Laws of Basic Commands -- 4.2 Algebraic Laws of Parallel Composition -- 5 Conclusion and Future Work -- References -- Reconciling Communication Delays and Negation -- 1 Introduction -- 2 Background -- 2.1 Continuous Queries over Datastreams in Temporal Datalog -- 2.2 Hypothetical Answers to Continuous Queries -- 2.3 Operational Semantics -- 2.4 Adding Negation -- 3 Declarative Semantics of Negation with Delays -- 4 Operational Semantics of Negation with Delays -- 4.1 The Evidence Lattice -- 4.2 The Negation Update Operator. 4.3 Soundness and Completeness -- 5 Computing the Operational Semantics -- 6 Related Work and Discussion -- References -- A Combinatorial Study of Async/Await Processes -- 1 Introduction -- 2 Async/Await Concurrency -- 3 Partial Order Decomposition and the Counting Problem -- 4 Chord Processes, Interval Orders and Related Families -- 5 Uniform Random Generation: Experimental Study -- 6 Conclusion and Future Work -- References -- Unsatisfiability of Comparison-Based Non-malleability for Commitments -- 1 Introduction -- 2 Comparison-Based Non-malleability -- 2.1 (Un)satisfiability of the Comparison-Based Definition -- 3 Conclusions -- References -- Alternating Automatic Register Machines -- 1 Introduction -- 2 Preliminaries -- 3 Alternating Automatic Register Machines -- 4 Polynomial-Size Padded Alternating Automatic Register Machine -- References -- Functional Choreographic Programming -- 1 Introduction -- 2 The Choreographic -calculus -- 2.1 Syntax -- 2.2 Typing -- 3 Semantics of Chor -- 4 Illustrative Examples -- 4.1 Secure Communication -- 4.2 EAP -- 5 Related Work -- 6 Conclusion and Future Work -- A Single Sign-on Authentication -- B Full Definitions and Proofs -- C Proof of Theorem 1 -- D Proof of Theorem 2 -- References -- A Model Checking Based Approach to Detect Safety-Critical Adversarial Examples on Autonomous Driving Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Model Checking with UPPAAL -- 2.2 Adversarial Examples Generation Algorithm -- 3 The Safety-Critical Adversarial Examples -- 4 Modelling the System and Detecting the SCAEs -- 4.1 Abstract Model of ADS in UPPAAL -- 4.2 Locating the Target and Timing -- 5 Experimental Evaluation -- 5.1 Experimental Setup -- 5.2 Selection of Traffic Map -- 5.3 Quantitative Performance -- 5.4 Analysis of the Experiment -- 6 Conclusion -- References. Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting -- 1 Introduction -- 2 Nominal Rewriting Systems with Atom-Variables -- 2.1 Preliminaries -- 2.2 Ground Nominal Terms -- 2.3 Nominal Term Expressions -- 2.4 Nominal Rewriting Systems with Atom-Variables -- 2.5 Overlaps -- 2.6 Parallel Reduction -- 3 Confluence Criteria by Strong Commutation -- 3.1 Proof Method for Confluence by Strong Commutation -- 3.2 Confluence Properties in Nominal Rewriting -- 3.3 A Sufficient Condition for Church-Rosser Modulo -equivalence -- 4 Conclusion -- References -- Local XOR Unification: Definitions, Algorithms and Application to Cryptography -- 1 Introduction -- 2 Preliminaries -- 3 Local XOR Unification -- 3.1 f-rooted Local Unification -- 3.2 -rooted Local Unification -- 4 Solving f-rooted Local Unification -- 4.1 Overview -- 4.2 Algorithm for Solving f-rooted Local Unification -- 5 Solving -rooted Local Unification -- 5.1 Overview -- 5.2 Handling Variables -- 5.3 Applying Inference Rules -- 5.4 -rooted Local Unification Procedure -- 6 Conclusion -- References -- A Matching Logic Foundation for Alk -- 1 Introduction -- 2 A Taste of Alk -- 3 Matching Logic Semantics of the Alk Language -- 3.1 A Short Introduction to Matching Logic -- 3.2 Alk Semantics in Matching Logic Terms -- 4 Behavioral Properties of Algorithms as ML Patterns -- 5 Implementation of the Verification Process -- 5.1 Deriving Reachability Patterns from Annotations -- 5.2 Proving Reachability Patterns by Symbolic Execution -- 5.3 Implementation -- 6 Related Work -- 7 Conclusion -- References -- A Type System with Subtyping for WebAssembly's Stack Polymorphism -- 1 Introduction -- 2 A Small Fragment of Wasm -- 3 Type System Dir with ``Direct'' Sequential Composition -- 4 Type System Sub with Qualifiers and Subtyping -- 5 Typed Big-Step Semantics Based on Sub. 6 An Improvement over Sub -- 7 Conclusions and Future Work -- References -- A Verified Implementation of B+-Trees in Isabelle/HOL -- 1 Introduction -- 2 Contributions -- 2.1 Related Work -- 3 B+-trees and Approach -- 3.1 Notation -- 3.2 Definitions -- 3.3 Implementation Definitions -- 3.4 Node Internal Navigation -- 4 Set Operations -- 4.1 Functional Point Query -- 4.2 Imperative Point Query -- 4.3 Insertion and Deletion -- 5 Range Operations -- 5.1 Iterators -- 5.2 Range Queries -- 6 Conclusion -- 6.1 Evaluation -- 6.2 Outlook -- References -- Active Learning for Deterministic Bottom-Up Nominal Tree Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Nominal Set -- 2.2 Data Tree -- 3 Deterministic Bottom-Up Nominal Tree Automata -- 4 Myhill-Nerode Theorem -- 5 Observation Table -- 6 Learning Algorithm -- 7 Example -- 8 Conclusion -- References -- Towards a User Interface Description Language Based on Bigraphs -- 1 Introduction -- 2 UIDLs -- 3 Bigraphs -- 3.1 Structural Aspect and Rewriting Rules -- 3.2 Bigraphical Reactive Systems (BRS) -- 4 Representation of Mechanisms with Bigraphs -- 4.1 Representation of the Scene Graph -- 4.2 GUI Interactions -- 4.3 Bigraphs Expressiveness -- 5 Bigraphs Verification -- 5.1 Predicats -- 5.2 Properties Verification on UI -- 6 Related and Future Work -- References -- A Specification Logic for Programs in the Probabilistic Guarded Command Language -- 1 Introduction -- 2 State of the Art -- 3 Preliminaries -- 4 pGCL: A Probabilistic Guarded Command Language -- 5 Probabilistic Dynamic Logic -- 6 The P-Box Modality and Logical Connectives -- 7 Expectations for Program Constructs -- 8 Purely Probabilistic and Deterministic Programs -- 9 Program Analysis with pDL -- 9.1 Monty Hall Game -- 9.2 Convergence of a Bernoulli Random Variable -- 10 Conclusion -- References. Card-Minimal Protocols for Symmetric Boolean Functions of More than Seven Inputs. |
| Record Nr. | UNISA-996495571003316 |
|
Seidl Helmut
|
||
| Cham, Switzerland : , : Springer International Publishing, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theoretical aspects of computing - ICTAC 2022 : 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, proceedings / / Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu
| Theoretical aspects of computing - ICTAC 2022 : 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, proceedings / / Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu |
| Autore | Seidl Helmut |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer International Publishing, , [2022] |
| Descrizione fisica | 1 online resource (494 pages) |
| Disciplina | 004 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer science
Computer science - Social aspects |
| ISBN | 3-031-17715-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- On Safety, Assurance and Reliability: A Software Engineering Perspective (Abstract of Invited Talk) -- Contents -- VeriMon: A Formally Verified Monitoring Tool -- 1 Introduction -- 2 Evolution -- 3 Future Directions -- 4 Discussion -- References -- Generalized Test Tables: A Domain-Specific Specification Language for Automated Production Systems -- 1 Introduction -- 2 The Domain of Automated Production Systems -- 3 Generalized Test Tables -- 4 Relational Test Tables -- 5 Conclusion -- References -- Reachability Games and Parity Games -- 1 Introduction -- 2 Games on Graphs -- 3 Reachability Games and Attractors -- 4 Optimal Strategies for Reachability Games -- 5 Parity Games -- 6 Zielonka's Algorithm for Parity Games -- 7 Lehtinen's Algorithm for Parity Games -- 8 Conclusion -- References -- Human-Cyber-Physical Automata and Their Synthesis -- 1 The Basic Model of HCPA -- 2 Synthesis of HCPS -- 3 Concluding Remarks -- References -- A PO Characterisation of Reconfiguration -- 1 Introduction -- 2 Labelled Partial Order Computations in a Nutshell -- 3 Preliminaries -- 3.1 Partial Orders and Labeled Partial Orders -- 3.2 Channelled Transition Systems (CTS) -- 3.3 Petri Nets with Inhibitor Arcs (PTI-nets) -- 4 LPO Semantics -- 4.1 Channelled Transition Systems (CTS) -- 4.2 Petri Nets with Inhibitor Arcs (PTI-nets) -- 5 Partial Order with Glue -- 5.1 Glue Computations for CTSs -- 5.2 Glue Computations for PTI-nets -- 6 Separating Choice and Forced Interleaving -- 6.1 Choice vs Reconfiguration-Forced Interleaving in CTSs -- 6.2 Choice vs Interleaving in PTI-nets -- 7 Concluding Remarks -- References -- Structural Rules and Algebraic Properties of Intersection Types -- 1 Introduction -- 2 Type Systems -- 3 Term Expansion -- 4 Conclusions -- References -- Quantitative Weak Linearisation -- 1 Introduction.
2 Terms and Reductions -- 3 Types -- 4 Weak-Linearisation for Strongly Normalising Terms -- 5 A Characterisation of Weak-Linear Terms -- 6 Related Works and Discussions -- 7 Conclusions and Future Work -- References -- On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems -- 1 Introduction -- 1.1 Related Work -- 2 Motivating Example Involving Drones -- 3 Timed Multiset Rewriting -- 4 Timed MSR for Resilient Systems -- 5 Verification Problems -- 6 Computational Complexity Results -- 7 Conclusions -- References -- Spatial and Timing Properties in Highway Traffic -- 1 Introduction -- 2 Preliminaries -- 2.1 Abstract Model of Motorway Traffic -- 2.2 Evolution of a Traffic Snapshot -- 2.3 MLSL with Scopes -- 2.4 State-Clock Logic -- 2.5 First-Order Theory of Real-Closed Fields -- 3 Timed MLSL -- 4 Semi-decision Procedure for TMLSL -- 5 Conclusion -- References -- Denotational and Algebraic Semantics for the CaIT Calculus -- 1 Introduction -- 2 The CaIT Calculus -- 2.1 Syntax -- 2.2 Guided Choice -- 3 Denotational Semantics -- 3.1 Semantic Model -- 3.2 Healthiness Conditions -- 3.3 Denotational Semantics of Basic Commands -- 3.4 Denotational Semantics of Guarded Choice -- 3.5 Parallel Composition -- 3.6 Channel Restriction -- 4 Algebraic Semantics -- 4.1 Algebraic Laws of Basic Commands -- 4.2 Algebraic Laws of Parallel Composition -- 5 Conclusion and Future Work -- References -- Reconciling Communication Delays and Negation -- 1 Introduction -- 2 Background -- 2.1 Continuous Queries over Datastreams in Temporal Datalog -- 2.2 Hypothetical Answers to Continuous Queries -- 2.3 Operational Semantics -- 2.4 Adding Negation -- 3 Declarative Semantics of Negation with Delays -- 4 Operational Semantics of Negation with Delays -- 4.1 The Evidence Lattice -- 4.2 The Negation Update Operator. 4.3 Soundness and Completeness -- 5 Computing the Operational Semantics -- 6 Related Work and Discussion -- References -- A Combinatorial Study of Async/Await Processes -- 1 Introduction -- 2 Async/Await Concurrency -- 3 Partial Order Decomposition and the Counting Problem -- 4 Chord Processes, Interval Orders and Related Families -- 5 Uniform Random Generation: Experimental Study -- 6 Conclusion and Future Work -- References -- Unsatisfiability of Comparison-Based Non-malleability for Commitments -- 1 Introduction -- 2 Comparison-Based Non-malleability -- 2.1 (Un)satisfiability of the Comparison-Based Definition -- 3 Conclusions -- References -- Alternating Automatic Register Machines -- 1 Introduction -- 2 Preliminaries -- 3 Alternating Automatic Register Machines -- 4 Polynomial-Size Padded Alternating Automatic Register Machine -- References -- Functional Choreographic Programming -- 1 Introduction -- 2 The Choreographic -calculus -- 2.1 Syntax -- 2.2 Typing -- 3 Semantics of Chor -- 4 Illustrative Examples -- 4.1 Secure Communication -- 4.2 EAP -- 5 Related Work -- 6 Conclusion and Future Work -- A Single Sign-on Authentication -- B Full Definitions and Proofs -- C Proof of Theorem 1 -- D Proof of Theorem 2 -- References -- A Model Checking Based Approach to Detect Safety-Critical Adversarial Examples on Autonomous Driving Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Model Checking with UPPAAL -- 2.2 Adversarial Examples Generation Algorithm -- 3 The Safety-Critical Adversarial Examples -- 4 Modelling the System and Detecting the SCAEs -- 4.1 Abstract Model of ADS in UPPAAL -- 4.2 Locating the Target and Timing -- 5 Experimental Evaluation -- 5.1 Experimental Setup -- 5.2 Selection of Traffic Map -- 5.3 Quantitative Performance -- 5.4 Analysis of the Experiment -- 6 Conclusion -- References. Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting -- 1 Introduction -- 2 Nominal Rewriting Systems with Atom-Variables -- 2.1 Preliminaries -- 2.2 Ground Nominal Terms -- 2.3 Nominal Term Expressions -- 2.4 Nominal Rewriting Systems with Atom-Variables -- 2.5 Overlaps -- 2.6 Parallel Reduction -- 3 Confluence Criteria by Strong Commutation -- 3.1 Proof Method for Confluence by Strong Commutation -- 3.2 Confluence Properties in Nominal Rewriting -- 3.3 A Sufficient Condition for Church-Rosser Modulo -equivalence -- 4 Conclusion -- References -- Local XOR Unification: Definitions, Algorithms and Application to Cryptography -- 1 Introduction -- 2 Preliminaries -- 3 Local XOR Unification -- 3.1 f-rooted Local Unification -- 3.2 -rooted Local Unification -- 4 Solving f-rooted Local Unification -- 4.1 Overview -- 4.2 Algorithm for Solving f-rooted Local Unification -- 5 Solving -rooted Local Unification -- 5.1 Overview -- 5.2 Handling Variables -- 5.3 Applying Inference Rules -- 5.4 -rooted Local Unification Procedure -- 6 Conclusion -- References -- A Matching Logic Foundation for Alk -- 1 Introduction -- 2 A Taste of Alk -- 3 Matching Logic Semantics of the Alk Language -- 3.1 A Short Introduction to Matching Logic -- 3.2 Alk Semantics in Matching Logic Terms -- 4 Behavioral Properties of Algorithms as ML Patterns -- 5 Implementation of the Verification Process -- 5.1 Deriving Reachability Patterns from Annotations -- 5.2 Proving Reachability Patterns by Symbolic Execution -- 5.3 Implementation -- 6 Related Work -- 7 Conclusion -- References -- A Type System with Subtyping for WebAssembly's Stack Polymorphism -- 1 Introduction -- 2 A Small Fragment of Wasm -- 3 Type System Dir with ``Direct'' Sequential Composition -- 4 Type System Sub with Qualifiers and Subtyping -- 5 Typed Big-Step Semantics Based on Sub. 6 An Improvement over Sub -- 7 Conclusions and Future Work -- References -- A Verified Implementation of B+-Trees in Isabelle/HOL -- 1 Introduction -- 2 Contributions -- 2.1 Related Work -- 3 B+-trees and Approach -- 3.1 Notation -- 3.2 Definitions -- 3.3 Implementation Definitions -- 3.4 Node Internal Navigation -- 4 Set Operations -- 4.1 Functional Point Query -- 4.2 Imperative Point Query -- 4.3 Insertion and Deletion -- 5 Range Operations -- 5.1 Iterators -- 5.2 Range Queries -- 6 Conclusion -- 6.1 Evaluation -- 6.2 Outlook -- References -- Active Learning for Deterministic Bottom-Up Nominal Tree Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Nominal Set -- 2.2 Data Tree -- 3 Deterministic Bottom-Up Nominal Tree Automata -- 4 Myhill-Nerode Theorem -- 5 Observation Table -- 6 Learning Algorithm -- 7 Example -- 8 Conclusion -- References -- Towards a User Interface Description Language Based on Bigraphs -- 1 Introduction -- 2 UIDLs -- 3 Bigraphs -- 3.1 Structural Aspect and Rewriting Rules -- 3.2 Bigraphical Reactive Systems (BRS) -- 4 Representation of Mechanisms with Bigraphs -- 4.1 Representation of the Scene Graph -- 4.2 GUI Interactions -- 4.3 Bigraphs Expressiveness -- 5 Bigraphs Verification -- 5.1 Predicats -- 5.2 Properties Verification on UI -- 6 Related and Future Work -- References -- A Specification Logic for Programs in the Probabilistic Guarded Command Language -- 1 Introduction -- 2 State of the Art -- 3 Preliminaries -- 4 pGCL: A Probabilistic Guarded Command Language -- 5 Probabilistic Dynamic Logic -- 6 The P-Box Modality and Logical Connectives -- 7 Expectations for Program Constructs -- 8 Purely Probabilistic and Deterministic Programs -- 9 Program Analysis with pDL -- 9.1 Monty Hall Game -- 9.2 Convergence of a Bernoulli Random Variable -- 10 Conclusion -- References. Card-Minimal Protocols for Symmetric Boolean Functions of More than Seven Inputs. |
| Record Nr. | UNINA-9910616203003321 |
|
Seidl Helmut
|
||
| Cham, Switzerland : , : Springer International Publishing, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||