Theory and Practice of Formal Methods
Springer International Publishing (Verlag)
9783319307336 (ISBN)
This Festschrift volume has been published in honor ofFrank de Boer, on the occasion of his 60th birthday.
Frank S. de Boer is a prominent member of the research community in formalmethods and theoretical computer science. A brief look at his lengthypublication list reveals a broad area of interest and a versatile modusoperandi with: logic and constraint programming; deductive proof systems,soundness, and completeness; semantics, compositionality, and full abstraction;process algebra and decidability; multithreading and actor-based concurrency;agent programming, ontologies, and modal logic; real-time systems, timedautomata, and schedulability; enterprise architectures, choreography, andcoordination; testing and runtime monitoring; and cloud computing and service-levelagreements. For a while, he also liked failures, especially in semantics, andoptimistically concluded with the failure of failures. In fact, Frank has anopportunistic approach to research. Rather than seeing obstacles, he findsopportunities.
Program Verification: to Err isHuman.-Fond (and Frank) Memories of Frank.- Warmest Congratulations, Frank.- ConformanceChecking of Real-Time Models: Symbolic Execution vs. Bounded Model Checking.- ResourceAnalysis of Distributed Systems.- Comparing Trace Expressions and LinearTemporal Logic for Runtime Verification.- Proper Protocol.- A CompositionalApproach to the Verification of Hybrid Systems.- Array Abstraction withSymbolic Pivots.- Modeling Role-Based Systems with Exogenous Coordination.- Vats:A Safe, Reactive Storage Abstraction.- Denotational and Operational Precisenessof Subtyping: A Roadmap.- A Sound and Complete Hoare Logic forDynamically-Typed, Object-Oriented Programs.- Self-ReconfiguringMicroservices.- Statically and Dynamically Verifiable SLA metrics.- EffectivelyEliminating Auxiliaries.- Towards a Proof Method for Paradigm.- Toward a FormalFoundation for Time Travel in Stories and Games.- Industrial Application ofFormal Models Generated from Domain SpecificLanguages.- Formal Verification ofOpen Normative Multi-Agent System.- Moessner's Theorem: An Exercise in CoinductiveReasoning in Coq.- Towards a Kool Future.- On the Expressiveness of Synchronizationin Component Deployment.- Characterisation of Simulation by ProbabilisticTesting.- On Time Actors.- A Small-Step Semantics of a Concurrent Calculus withGoroutines and Deferred Functions.- Quicksort Revisited - Verifying AlternativeVersions of Quicksort.
| Erscheinungsdatum | 08.10.2016 |
|---|---|
| Reihe/Serie | Lecture Notes in Computer Science | Theoretical Computer Science and General Issues |
| Zusatzinfo | XII, 427 p. 112 illus. in color. |
| Verlagsort | Cham |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Themenwelt | Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge |
| Mathematik / Informatik ► Informatik ► Software Entwicklung | |
| Informatik ► Theorie / Studium ► Algorithmen | |
| Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik | |
| Schlagworte | Abstract Interpretation • Actor Model • Algorithm analysis and problem complexity • algorithms • array abstraction • artificial intelligence (incl. robotics) • Automated Verification • axiomatic semantics • completeness for total correctness • dynamic typing • Logics and meanings of programs • loop invariant generation • Mathematical logic and formal languages • Microservices • multiple notions of correctness • Programming languages, compilers, interpreters • program transformation and verification • pure object-orientation • Quicksort • reduction technique • relative completeness • runtime verification • Service-Oriented Architecture • Software engineering • Software Engineering / Softwareentwicklung • soundness • tagged hoare logic |
| ISBN-13 | 9783319307336 / 9783319307336 |
| Zustand | Neuware |
| Informationen gemäß Produktsicherheitsverordnung (GPSR) | |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
