Software engineering and formal methods : 20th International Conference, SEFM 2022, Berlin, Germany, September 26-30, 2022, proceedings / / Bernd-Holger Schlingloff and Ming Chai, editors

• Pubblicazione: Cham, Switzerland : , : Springer, , [2022]; ©2022
• Descrizione fisica: 1 online resource (373 pages)
• Disciplina: 004.0151
• Soggetto topico: Formal methods (Computer science); Software engineering
• Persona (resp. second.): SchlingloffBernd-Holger; ChaiMing
• Nota di contenuto: Intro -- Preface -- Organization -- Invited Talks -- Distributed Process Calculi with Local States -- Maintenance Meets Model Checking-Predictive Maintenance via Fault Trees and Formal Methods -- Towards Verifying Neural-Symbolic Multi-Agent Systems -- Contents -- Software Verification -- A Unifying Approach for Control-Flow-Based Loop Abstraction -- 1 Introduction -- 2 Preliminaries -- 3 Loop Abstractions -- 3.1 Theory -- 3.2 Combining Strategies for Loop Abstraction -- 4 Evaluation -- 4.1 Benchmark Environment -- 4.2 Experiments -- 5 Conclusion -- References -- Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers -- 1 Introduction -- 2 Our Proving Process Steps -- 2.1 Generating and Processing Verification Conditions -- 2.2 Simplifications and Bounds Derivation -- 2.3 Eliminating Floating-Point Operations -- 3 Deriving Provable Error Bounds -- 4 Verification of Heron's Method for Approximating the Square Root Function -- 5 Verifying AdaCore's Sine Implementation -- 6 Benchmarking the Proving Process -- 6.1 Counter-examples -- 7 Conclusion -- References -- Information Exchange Between Over- and Underapproximating Software Analyses -- 1 Introduction -- 2 Background -- 2.1 Program Syntax and Semantics -- 2.2 Existing Artifacts -- 3 Validation Artifact GIA -- 4 Using GIAs in Cooperative Validation -- 5 Implementation and Evaluation -- 6 Conclusion -- References -- Program Analysis -- A Query Language for Language Analysis -- 1 Introduction -- 2 Languages as Databases -- 3 The Lang-SQL Query Language -- 4 Rewriting Lang-n-Check as Lang-SQL Queries -- 5 Evaluation -- 6 Related Work -- 7 Conclusion -- References -- Field-Sensitive Program Slicing -- 1 Introduction -- 2 Slicing Composite Data Structures -- 3 Constrained-Edges Program Dependence Graph -- 3.1 Extending the PDG -- 3.2 Slicing the CE-PDG: Constrained Traversal. ; 3.3 The Slicing Algorithm -- 3.4 Dealing with Loops -- 4 Implementation and Empirical Evaluation -- 5 Related Work -- 6 Conclusion -- References -- SPouT: Symbolic Path Recording During Testing - A Concolic Executor for the JVM -- 1 Introduction -- 2 SPouT: Directing the Flow of Espresso -- 2.1 SPouT's Design -- 2.2 Memory Architecture -- 2.3 Symbolic Encoding of String Operations -- 2.4 Supported Languages and Implemented Features -- 3 Demonstration and Evaluation -- 4 Conclusion -- References -- Verifier Technology -- Cooperation between Automatic and Interactive Software Verifiers -- 1 Introduction -- 2 Preliminaries -- 2.1 Verification Witnesses -- 2.2 ACSL -- 3 A Component Framework for Cooperative Verification -- 3.1 Witness2ACSL -- 3.2 ACSL2Witness -- 3.3 Witness2Assert -- 4 Evaluation -- 4.1 Experimental Setup -- 4.2 Benchmark Set with Useful Witnesses -- 4.3 Experimental Results -- 4.4 Case Study on Interactive Verification with Manual Annotations -- 5 Conclusion -- References -- Strategy Switching: Smart Fault-Tolerance for Weakly-Hard Resource-Constrained Real-Time Applications -- 1 Introduction -- 2 System Models -- 3 A State Machine of Strategies -- 4 Strategy State Machine Construction -- 4.1 Enumerating Strategies and Results -- 4.2 Strategy Linking -- 4.3 State Machine Construction Algorithm -- 4.4 Algorithmic Complexity -- 5 Evaluating State Machines -- 5.1 Discrete-Time Markov Chain Evaluation -- 6 Evaluation -- 6.1 Dataset -- 6.2 Results -- 7 Validation Using UPPAAL -- 7.1 UPPAAL Processes -- 7.2 Validating Results -- 8 Related Work -- 9 Conclusion -- 10 Future Work -- References -- A Program Slicer for Java (Tool Paper) -- 1 Introduction -- 2 Background -- 3 Producing Slices with JavaSlicer -- 3.1 Slicing More Than One File -- 3.2 Slicing with External Libraries -- 4 Implementation -- 5 Empirical Evaluation -- 6 Related Work. ; 7 Conclusions -- References -- Formal Methods for Intelligent and Learning Systems -- Constrained Training of Recurrent Neural Networks for Automata Learning -- 1 Introduction -- 2 Preliminaries -- 2.1 Recurrent Neural Networks -- 2.2 Finite State Machines -- 2.3 Automata Learning -- 3 Automata Learning with RNNs -- 3.1 Overview and Architecture -- 3.2 Training and Automaton Extraction -- 4 Case Studies -- 4.1 Case Study Subjects -- 4.2 Experimental Setup -- 4.3 Results and Discussion -- 5 Related Work -- 6 Conclusion -- References -- Neural Network Verification Using Residual Reasoning -- 1 Introduction -- 2 Background -- 3 Residual Reasoning (RR) -- 4 Residual Reasoning and Neuron-Merging Abstraction -- 5 Adding Residual Reasoning to Reluplex -- 6 Experiments and Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Training Agents to Satisfy Timed and Untimed Signal Temporal Logic Specifications with Reinforcement Learning -- 1 Introduction -- 2 Preliminaries -- 2.1 (Deep) Reinforcement Learning -- 2.2 Signal Temporal Logic -- 3 Examples -- 3.1 Pendulum -- 3.2 CartPole -- 4 Our Approach: STLGym -- 4.1 Computing the Robustness Degree -- 4.2 Allowable Specifications -- 4.3 Calculating Reward -- 5 Example Case Studies -- 5.1 Sparse vs Dense Reward -- 5.2 STLGym is Algorithm-Agnostic -- 5.3 On Separating Specifications and Scaling -- 5.4 Retraining with New Goal -- 5.5 Learning a Timed Specification -- 6 Related Work -- 6.1 Quantitative Semantics -- 6.2 Reward Machines -- 7 Conclusions and Future Work -- References -- Specification and Contracts -- Information Flow Control-by-Construction for an Object-Oriented Language -- 1 Introduction -- 2 Object-Oriented Language SIFO by Example -- 3 IFbCOO by Example -- 4 Formalizing Information Flow Control-by-Construction -- 4.1 Core Calculus of SIFO -- 4.2 Refinement Rules for Program Construction. ; 4.3 Proof of Soundness -- 5 CorC Tool Support and Evaluation -- 5.1 CorC for IFbCOO -- 5.2 Case Studies and Discussion -- 6 Related Work -- 7 Conclusion -- References -- Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts -- 1 Introduction -- 2 Background -- 2.1 Solidity -- 2.2 Formal Verification with solc-verify -- 3 Safe Ethereum Smart Contracts Deployment -- 3.1 Verifier -- 3.2 Upgrader -- 4 Case Studies: ERC20, ERC1155, and ERC3156 -- 5 Related Work -- 6 Conclusion -- References -- SKLEE: A Dynamic Symbolic Analysis Tool for Ethereum Smart Contracts (Tool Paper) -- 1 Introduction -- 2 Overview of SKLEE -- 2.1 Contract Translator -- 2.2 Augmenting KLEE -- 2.3 Vulnerabilities and Their Detection -- 2.4 Validation -- 2.5 Limitations -- 3 Experiments and Results -- 4 Conclusion -- References -- Program Synthesis -- Weighted Games for User Journeys -- 1 Introduction -- 2 Preliminaries -- 3 From User Logs to Games -- 4 Capturing User Feedback in User Journey Games -- 5 Finite Unrolling of Games -- 6 Model Checking User Journeys -- 7 Implementing the Pipeline to Analyse User Journeys -- 8 Evaluating the Analysis Pipeline -- 8.1 Context -- 8.2 Observations in the Weighted Game -- 8.3 Model Checking the Case Study -- 8.4 Recommendations from the Observations and Analysis -- 9 Conclusions and Future Work -- References -- Safety Controller Synthesis for a Mobile Manufacturing Cobot -- 1 Introduction -- 2 Manufacturing Process -- 3 Safety Controller Synthesis -- 3.1 Overview of the Approach -- 3.2 Stage 1: Hazard Identification -- 3.3 Stage 2: Stochastic Modelling -- 3.4 Stage 3: Synthesis -- 4 Evaluation -- 4.1 Generation of Safety Controller Instantiations -- 4.2 Evaluation on a Digital Twin -- 5 Related Work -- 6 Conclusion -- References -- Timely Specification Repair for Alloy 6 -- 1 Introduction -- 2 Related Work. ; 3 Alloy Temporal Repair -- 3.1 Overview -- 3.2 Mutation-Based Repair with Counterexample-Based Pruning -- 3.3 Implementation Details -- 4 Evaluation -- 5 Conclusions -- References -- Temporal Logic -- BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees -- 1 Introduction -- 1.1 Background -- 1.2 The Blackboard -- 2 Related Work -- 2.1 Strengths and Uses of BTs -- 2.2 Expanded BTs -- 2.3 Verification of BTs -- 3 Overview of Approach -- 4 Encodings -- 4.1 Leaf -- 4.2 Total -- 4.3 BTCompiler -- 5 Results -- 5.1 Checklist and Parallel-Checklist -- 5.2 BlueROV -- 6 Conclusions and Future Work -- References -- CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper) -- 1 Introduction -- 2 Tool Data Flow of CHA -- 3 Case Studies -- 3.1 GCD Module with 4-Bits Inputs -- 3.2 Wishbone Interface -- 4 Conclusion and Future Work -- References -- Runtime Methods -- Runtime Verification with Imperfect Information Through Indistinguishability Relations -- 1 Introduction -- 2 Preliminaries -- 3 Runtime Verification with Imperfect Information -- 3.1 How Can We Formally Represent the Imperfect Information? -- 3.2 Re-engineering Monitor with Imperfect Information -- 4 Implementation -- 4.1 Remote Inspection Case Study -- 4.2 Experimental Results -- 5 Related Work -- 6 Conclusions and Future Work -- References -- Runtime Enforcement for IEC 61499 Applications -- 1 Introduction -- 2 Background -- 2.1 IEC 61499 -- 2.2 Runtime Enforcement -- 2.3 Running Example -- 3 Runtime Enforcement Techniques -- 3.1 Enforcement Architecture -- 3.2 Property Automaton -- 3.3 Enforcer Synthesis -- 3.4 Enforcer Integration -- 3.5 Characteristics -- 4 Tool Support -- 5 Related Work -- 6 Concluding Remarks -- References -- Author Index.
• Titolo autorizzato: Software Engineering and Formal Methods
• ISBN: 3-031-17108-X
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910595023603321
• Lo trovi qui: Univ. Federico II
• Serie: Lecture notes in computer science.