000851717 000__ 04500cam\a2200445Mu\4500
000851717 001__ 851717
000851717 005__ 20230306145208.0
000851717 006__ m\\\\\o\\d\\\\\\\\
000851717 007__ cr\un\nnnunnun
000851717 008__ 181103s2018\\\\xx\\\\\\o\\\\\010\0\eng\d
000851717 020__ $$a9783319980478$$q(electronic book)
000851717 020__ $$a3319980475$$q(electronic book)
000851717 020__ $$z9783319980461
000851717 035__ $$aSP(OCoLC)on1061128721
000851717 035__ $$aSP(OCoLC)1061128721
000851717 040__ $$aEBLCP$$beng$$cEBLCP$$dGW5XE
000851717 049__ $$aISEA
000851717 050_4 $$aQA76.76.D47
000851717 08204 $$a005.1$$223
000851717 24500 $$aPrincipled software development :$$bessays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday /$$cPeter Müller, Ina Schaefer, editors.
000851717 260__ $$aCham :$$bSpringer,$$c2018.
000851717 300__ $$a1 online resource (326 pages)
000851717 336__ $$atext$$btxt$$2rdacontent
000851717 337__ $$acomputer$$bc$$2rdamedia
000851717 338__ $$aonline resource$$bcr$$2rdacarrier
000851717 5050_ $$aIntro; 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
000851717 5058_ $$a2 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
000851717 5058_ $$a4 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
000851717 5058_ $$aA 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
000851717 5058_ $$aCompositional 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
000851717 506__ $$aAccess limited to authorized users.
000851717 588__ $$aDescription based upon print version of record.
000851717 650_0 $$aComputer software$$xDevelopment.
000851717 7001_ $$aMüller, Peter.
000851717 7001_ $$aSchaefer, Ina.
000851717 77608 $$iPrint version:$$aMüller, Peter$$tPrincipled Software Development : Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of His 60th Birthday$$dCham : Springer,c2018$$z9783319980461
000851717 852__ $$bebk
000851717 85640 $$3SpringerLink$$uhttps://univsouthin.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-319-98047-8$$zOnline Access$$91397441.1
000851717 909CO $$ooai:library.usi.edu:851717$$pGLOBAL_SET
000851717 980__ $$aEBOOK
000851717 980__ $$aBIB
000851717 982__ $$aEbook
000851717 983__ $$aOnline
000851717 994__ $$a92$$bISE