06879nam 22007935 450 99646578120331620230221150157.01-280-38785-897866135657783-642-14295-810.1007/978-3-642-14295-6(CKB)2550000000015596(SSID)ssj0000446364(PQKBManifestationID)11297669(PQKBTitleCode)TC0000446364(PQKBWorkID)10492148(PQKB)10580752(DE-He213)978-3-642-14295-6(MiAaPQ)EBC3065505(PPN)149072821(EXLCZ)99255000000001559620100709d2010 u| 0engurnn|008mamaatxtccrComputer Aided Verification[electronic resource] 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings /edited by Tayssir Touili, Byron Cook, Paul Jackson1st ed. 2010.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2010.1 online resource (XVI, 676 p. 169 illus.) Theoretical Computer Science and General Issues,2512-2029 ;6174Bibliographic Level Mode of Issuance: Monograph3-642-14294-X Includes bibliographical references and index.Invited Talks -- Policy Monitoring in First-Order Temporal Logic -- Retrofitting Legacy Code for Security -- Quantitative Information Flow: From Theory to Practice? -- Memory Management in Concurrent Algorithms -- Invited Tutorials -- ABC: An Academic Industrial-Strength Verification Tool -- There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code -- Constraint Solving for Program Verification: Theory and Practice by Example -- Session 1. Software Model Checking -- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data -- Termination Analysis with Compositional Transition Invariants -- Lazy Annotation for Program Testing and Verification -- The Static Driver Verifier Research Platform -- Dsolve: Safety Verification via Liquid Types -- Contessa: Concurrency Testing Augmented with Symbolic Analysis -- Session 2. Model Checking and Automata -- Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing -- Efficient Emptiness Check for Timed Büchi Automata -- Session 3. Tools -- Merit: An Interpolating Model-Checker -- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems -- Jtlv: A Framework for Developing Verification Algorithms -- Petruchio: From Dynamic Networks to Nets -- Session 4. Counter and Hybrid Systems Verification -- Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems -- Safety Verification for Probabilistic Hybrid Systems -- A Logical Product Approach to Zonotope Intersection -- Fast Acceleration of Ultimately Periodic Relations -- An Abstraction-Refinement Approach to Verification of Artificial Neural Networks -- Session 5. Memory Consistency -- Fences in Weak Memory Models -- Generating Litmus Tests for Contrasting Memory Consistency Models -- Session 6. Verification of Hardware and Low Level Code -- Directed Proof Generation for Machine Code -- Verifying Low-Level Implementations of High-Level Datatypes -- Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics -- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification -- Session 7. Tools -- LTSmin: Distributed and Symbolic Reachability -- libalf: The Automata Learning Framework -- Session 8. Synthesis -- Symbolic Bounded Synthesis -- Measuring and Synthesizing Systems in Probabilistic Environments -- Achieving Distributed Control through Model Checking -- Robustness in the Presence of Liveness -- RATSY – A New Requirements Analysis Tool with Synthesis -- Comfusy: A Tool for Complete Functional Synthesis -- Session 9. Concurrent Program Verification I -- Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs -- Automatically Proving Linearizability -- Model Checking of Linearizability of Concurrent List Implementations -- Local Verification of Global Invariants in Concurrent Programs -- Abstract Analysis of Symbolic Executions -- Session 10. Compositional Reasoning -- Automated Assume-Guarantee Reasoning through Implicit Learning -- Learning Component Interfaces with May and Must Abstractions -- A Dash of Fairness for Compositional Reasoning -- SPLIT: A Compositional LTL Verifier -- Session 11. Tools -- A Model Checker for AADL -- PESSOA: A Tool for Embedded Controller Synthesis -- Session 12. Decision Procedures -- On Array Theory of Bounded Elements -- Quantifier Elimination by Lazy Model Enumeration -- Session 13. Concurrent Program Verification II -- Bounded Underapproximations -- Global Reachability in Bounded Phase Multi-stack Pushdown Systems -- Model-Checking Parameterized Concurrent Programs Using Linear Interfaces -- Dynamic Cutoff Detection in Parameterized Concurrent Programs -- Session 14. Tools -- PARAM: A Model Checker for Parametric Markov Models -- Gist: A Solver for Probabilistic Games -- A NuSMV Extension for Graded-CTL Model Checking.Theoretical Computer Science and General Issues,2512-2029 ;6174Computer scienceSoftware engineeringCompilers (Computer programs)Machine theoryArtificial intelligenceComputer networksComputer Science Logic and Foundations of ProgrammingSoftware EngineeringCompilers and InterpretersFormal Languages and Automata TheoryArtificial IntelligenceComputer Communication NetworksComputer science.Software engineering.Compilers (Computer programs).Machine theory.Artificial intelligence.Computer networks.Computer Science Logic and Foundations of Programming.Software Engineering.Compilers and Interpreters.Formal Languages and Automata Theory.Artificial Intelligence.Computer Communication Networks.005.1015113Touili Tayssiredthttp://id.loc.gov/vocabulary/relators/edtCook Byronedthttp://id.loc.gov/vocabulary/relators/edtJackson Pauledthttp://id.loc.gov/vocabulary/relators/edtBOOK996465781203316Computer Aided Verification772228UNISA04017 am 22005053u 450 991013081650332120230617034312.0(CKB)3450000000002817(SSID)ssj0000985824(PQKBManifestationID)11985357(PQKBTitleCode)TC0000985824(PQKBWorkID)10932887(PQKB)10967881(OCoLC)808383323(WaSeSS)Ind00074082(EXLCZ)99345000000000281720160829h20042004 uy 0gerurmn#nnn|||||txtrdacontentcrdamediacrrdacarrierDas Buch der Bücher seine Wirkungsgeschichte in der Literatur /Tom Kleffmann (Hg.)Göttingen :Universitätsverlag Göttingen,2004.©20041 online resource (175 pages) digital, PDF file(s)Cycle of lectures given Sept.-Nov. 2003 at the St. Jacobi-Kirche, Göttingen, Germany.Print version: 3930457598 Includes bibliographical references."Hiob, o Hiob! Sprachst du wirklich nichts anderes als diese Worte?" : das Buch Hiob und die Literatur / Gerhard Lauer -- Eine weithin unbekannte Schöne : die lateinische Bibelepik der Spätantike / Siegmar Döpp -- Die Bibel in der französischen Literatur : Voltaire, Gide, Giraudoux / Jürgen von Stackelberg -- "Die Vertreibung aus dem Paradies" : der Ursprungsmythos (Genesis 3) als Herausforderung in Philosophie und Literatur der Neuzeit / Jürgen Gidion -- Shakespeare und die Bibel / Theodor Wolpers -- Die Heilige Schrift und die Schriftstellerei in Amerika : der Fall Melville / Daniel Göske -- "Ein Fest der Erzählung" : Thomas Manns Romanzyklus Joseph und seine Brüder / Irmela von der Lühe -- Wiederkehrender und revolutionärer Christus in der russischen Literatur / Reinhard Lauer.The firms and markets of today's complex socio-economic system developed in a spontaneous process termed evolution, in just the same way as the universe, the solar system, the Earth and all that lives upon it. Darwin's theory of evolution clearly demonstrated that evolution involved increasing organization. As we began to explore the molecular basis of life and its evolution, it became equally clear that it depended on the processing and communication of information. This book develops a consistent theory of evolution in its wider sense, examining the information based laws and forces that drive it. Exploring subjects as diverse as economics and the theories of thermodynamics, the author revisits the paradox of the apparent conflict between the laws of thermodynamics and evolution to arrive at a systems theory, tracing a continuous line of evolving information sets that connect the Big-Bang to the firms and markets of our current socio-economic system.Im Jahr 2003 fand in der Göttinger Jakobikirche eine hochkarätige und deshalb zu Recht viel beachtete Vorlesungsreihe zur Wirkungsgeschichte der Bibel statt. Namhafte Vertreter bester Göttinger Philologie fanden hier ihr Publikum - interessiert, oft gelehrt, aber in seinem Interesse nicht auf eine fachwissenschaftliche Binnendiskussion beschränkt. Diese nun gedruckt vorliegende Vorlesungsreihe ist nicht nur ein Beispiel für das gute Zusammenleben von Universität und Stadt, wie es typisch für Göttingen ist. Sie ist darüberhinaus Beispiel für ein fruchtbares Gespräch zwischen Wissenschaft und Kirche, wie es auch außerhalb der akademischen Theologie möglich und nötig ist.Bible and literatureTheology, PracticalBible and literature.Theology, Practical.809.93522Kleffmann TomPQKBAuAdUSAUkMaJRUBOOK9910130816503321Das Buch der Bücher2107128UNINA