Linked e-resources
Details
Table of Contents
Intro; Preface; Contents; Smart Contracts: A Killer Application for Deductive Source Code Verification; 1 The Blockchain and Smart Contracts; 2 Faulty Smart Contracts; 3 Approaches to Smart Contract Verification: The Landscape; 4 Towards a Deductive Source Code Verifier for Smart Contracts; 4.1 Challenges; 4.2 Approach; 5 Discussion; References; A Methodology for Invariants, Framing, and Subtyping in JML; 1 Introduction; 1.1 Framing Problems and Our Solutions; 1.1.1 Dynamically-Allocated Memory; 1.1.2 Object Invariants; 1.1.3 Dynamic Method Calls; 1.2 Contribution; 1.3 Outline
2 Dynamic Frames in JML2.1 New Type region; 2.2 Supporting Separating Conjunction; 2.3 A Read Effect Function; 2.4 Example; 3 Object Invariants; 4 Dynamic Method Calls; 5 Related Work; 6 Conclusion; References; Trends in Relational Program Verification; 1 Introduction; 2 Basic Notions and Definitions; 3 Application Scenarios; 3.1 Single-Program Properties; 3.1.1 Non-interference and Information-Flow Properties; 3.1.2 Symmetry Properties; 3.2 Multi-Program Properties; 3.2.1 Regression Verification; 3.2.2 Translation Validation; 3.2.3 Contextual Equivalence; 3.2.4 Refinement
4 Verification of Relational Properties4.1 Reduction to Functional Verification; 4.2 Exploiting Similarity Between Program Runs; 4.3 More Elaborate Synchronisation Schemes; 4.4 Alternative Approaches; 5 Conclusions; References; Collaborative Work Management with a Highly-Available Kanban Board; Prelude; 1 Introduction; 2 System Model; 3 Formal Model of a Kanban Board; 3.1 Data Model; 3.2 Operations; Interlude; 4 On Correctness of the Model; 5 From Model to Implementation; 5.1 Working with Inconsistencies and Invariants; Postlude; References
A Case for Certifying Compilers in Industrial Automation1 Introduction; Overview; 2 Certifying Compilers vs. Compiler Verification; 2.1 Semantics; 2.2 Trusted Computing Base; 2.3 Verified Compilers; 2.4 Certifying Compilers; 3 Software Development for Industrial Automation; 3.1 Programmable Logic Controllers; 3.2 IEC 61131-3; 3.3 IEC 61499; 4 Compilation Correctness in Industrial Automation; 4.1 Compilation Correctness as a "Low Hanging" Fruit; 4.2 Challenges for PLC Verification; 4.3 Benefits and Additional Research Challenges; 5 Conclusion; References
Compositional Semantics for Concurrent Object Groups in ABS1 Introduction; 2 Preliminaries; 3 Thread Semantics; 4 Semantics of Concurrent Object Groups; 5 Semantics of Systems of Concurrent Object Groups; 6 Trace Semantics; 7 Future Work; References; Same Same But Different: Interoperability of Software Product Line Variants; 1 Introduction; 2 Featherweight Core ABS with Modules; 3 Delta-Oriented VPLs; 3.1 Variant-Interoperable Product Lines; 3.2 Syntax; 3.3 A VPL for Railway Signals; 3.4 Glue Program Flattening for FDAM; 4 Delta-Oriented DVPLs; 4.1 Syntax; 4.2 A DVPL for Railway Stations; 4.3 Glue Program Flattening for FDDAM
2 Dynamic Frames in JML2.1 New Type region; 2.2 Supporting Separating Conjunction; 2.3 A Read Effect Function; 2.4 Example; 3 Object Invariants; 4 Dynamic Method Calls; 5 Related Work; 6 Conclusion; References; Trends in Relational Program Verification; 1 Introduction; 2 Basic Notions and Definitions; 3 Application Scenarios; 3.1 Single-Program Properties; 3.1.1 Non-interference and Information-Flow Properties; 3.1.2 Symmetry Properties; 3.2 Multi-Program Properties; 3.2.1 Regression Verification; 3.2.2 Translation Validation; 3.2.3 Contextual Equivalence; 3.2.4 Refinement
4 Verification of Relational Properties4.1 Reduction to Functional Verification; 4.2 Exploiting Similarity Between Program Runs; 4.3 More Elaborate Synchronisation Schemes; 4.4 Alternative Approaches; 5 Conclusions; References; Collaborative Work Management with a Highly-Available Kanban Board; Prelude; 1 Introduction; 2 System Model; 3 Formal Model of a Kanban Board; 3.1 Data Model; 3.2 Operations; Interlude; 4 On Correctness of the Model; 5 From Model to Implementation; 5.1 Working with Inconsistencies and Invariants; Postlude; References
A Case for Certifying Compilers in Industrial Automation1 Introduction; Overview; 2 Certifying Compilers vs. Compiler Verification; 2.1 Semantics; 2.2 Trusted Computing Base; 2.3 Verified Compilers; 2.4 Certifying Compilers; 3 Software Development for Industrial Automation; 3.1 Programmable Logic Controllers; 3.2 IEC 61131-3; 3.3 IEC 61499; 4 Compilation Correctness in Industrial Automation; 4.1 Compilation Correctness as a "Low Hanging" Fruit; 4.2 Challenges for PLC Verification; 4.3 Benefits and Additional Research Challenges; 5 Conclusion; References
Compositional Semantics for Concurrent Object Groups in ABS1 Introduction; 2 Preliminaries; 3 Thread Semantics; 4 Semantics of Concurrent Object Groups; 5 Semantics of Systems of Concurrent Object Groups; 6 Trace Semantics; 7 Future Work; References; Same Same But Different: Interoperability of Software Product Line Variants; 1 Introduction; 2 Featherweight Core ABS with Modules; 3 Delta-Oriented VPLs; 3.1 Variant-Interoperable Product Lines; 3.2 Syntax; 3.3 A VPL for Railway Signals; 3.4 Glue Program Flattening for FDAM; 4 Delta-Oriented DVPLs; 4.1 Syntax; 4.2 A DVPL for Railway Stations; 4.3 Glue Program Flattening for FDDAM