LEADER 01874nam 2200409 n 450 001 996391259003316 005 20200824121652.0 035 $a(CKB)4940000000104982 035 $a(EEBO)2240906674 035 $a(UnM)99853358e 035 $a(UnM)99853358 035 $a(EXLCZ)994940000000104982 100 $a19920612d1614 uy | 101 0 $aeng 135 $aurbn||||a|bb| 200 02$aA treatise concerning the ground of faith. VVritten in Latin, by the reuerend Father Iames Gordon Huntley of Scotland, Doctour of Diuinity, of the Society of Iesus. And translated into English, by I.L. of the same Society. The second part of the second controuersy$b[electronic resource] 210 $a[Saint-Omer $cPrinted at the English College Press] Permissu superiorum$dM.DC.XIV [1614] 215 $a68 p 300 $aI.L. = William Wright. 300 $aA translation of the second part of the second controversy in Gordon, James. Controversiarum epitomes. 300 $aPlace of publication and name of press from STC. 300 $aReproduction of the original in the Cambridge University Library. 330 $aeebo-0021 606 $aChurch$xAuthority$vEarly works to 1800 606 $aChurch$xInfallibility$vEarly works to 1800 615 0$aChurch$xAuthority 615 0$aChurch$xInfallibility 700 $aGordon$b James$f1541-1620.$01004861 701 $aWright$b William$f1563-1639.$01003408 801 0$bCu-RivES 801 1$bCu-RivES 801 2$bCStRLIN 801 2$bWaOLN 906 $aBOOK 912 $a996391259003316 996 $aA treatise concerning the ground of faith. VVritten in Latin, by the reuerend Father Iames Gordon Huntley of Scotland, Doctour of Diuinity, of the Society of Iesus. And translated into English, by I.L. of the same Society. The second part of the second controuersy$92334952 997 $aUNISA LEADER 11149nam 22008655 450 001 9910484890903321 005 20251226203628.0 010 $a3-319-26287-4 024 7 $a10.1007/978-3-319-26287-1 035 $a(CKB)4340000000001202 035 $a(SSID)ssj0001585171 035 $a(PQKBManifestationID)16265153 035 $a(PQKBTitleCode)TC0001585171 035 $a(PQKBWorkID)14866040 035 $a(PQKB)11274469 035 $a(DE-He213)978-3-319-26287-1 035 $a(MiAaPQ)EBC6284756 035 $a(MiAaPQ)EBC5610368 035 $a(Au-PeEL)EBL5610368 035 $a(OCoLC)1078998485 035 $a(PPN)190529458 035 $a(EXLCZ)994340000000001202 100 $a20151026d2015 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aHardware and Software: Verification and Testing $e11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings /$fedited by Nir Piterman 205 $a1st ed. 2015. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2015. 215 $a1 online resource (XVI, 293 p. 88 illus. in color.) 225 1 $aProgramming and Software Engineering,$x2945-9168 ;$v9434 300 $aIncludes index. 311 08$a3-319-26286-6 327 $aIntro -- Preface -- Organization -- Invited Talks -- Hybrid Systems -- Between Testing and Verification: Software Model Checking via Systematic Testing -- Fight for the Future of Verification -- Live in it Today -- Between Art and Craft: The Self-conception of a Verification Engineer -- Reasoning About Program Data Structure Shape: From the Heap to Distributed Systems -- Contents -- XSpeed: Accelerating Reachability Analysis on Multi-core Processors -- 1 Introduction -- 2 Preliminaries -- 2.1 Support Functions -- 2.2 Reachability Analysis Using Support Functions -- 3 Parallel State-Space Exploration -- 3.1 Parallel Samplings over Template Directions -- 3.2 Parallel Exploration of Reachable States -- 4 Sampling Support Functions in GPU -- 4.1 CUDA Programming Model -- 4.2 Computing Support Functions of Polytopes in GPU -- 4.3 Computing Support Functions of Hyperbox in GPU -- 5 Experiments -- 5.1 Five Dimensional System -- 5.2 Helicopter Controller -- 6 Conclusion -- References -- Abstraction-Based Parameter Synthesis for Multiaffine Systems -- 1 Introduction -- 2 Preliminaries -- 3 Abstraction of MHA -- 3.1 Pointwise LHA Abstraction -- 3.2 Set-Based LHA Abstraction -- 4 Hierarchical Parameter Search -- 4.1 Computation of Underapproximative Abstractions -- 4.2 Discrete Abstraction of MHA -- 4.3 Parameter Identification -- 5 Evaluation -- 6 Related Work -- 7 Conclusion -- References -- Tools -- Combining Static and Dynamic Analyses for Vulnerability Detection: Illustration on Heartbleed -- 1 Introduction -- 2 The Heartbleed Vulnerability -- 3 Overview of the Flinder-SCA Tool -- 4 Detection of Alarms by Static Analysis -- 5 Simplification of the Program by Slicing -- 6 Confirmation of Alarms by Fuzz Testing -- 7 Tool Demonstration -- 7.1 Static Analysis Step Applied to the Heartbleed Vulnerability. 327 $a7.2 Fuzz Testing Step Applied to the Heartbleed Vulnerability -- 8 Discussion -- 9 Conclusion and Future Work -- References -- The Verification Cockpit -- Creating the Dream Playground for Data Analytics over the Verification Process -- 1 Introduction -- 2 Motivation and Goals -- 3 Architecture and Implementation of the Verification Cockpit -- 3.1 Architecture of the Verification Cockpit -- 3.2 The Data Model -- 3.3 Implementation -- 4 Use Examples -- 4.1 Test Submission Dashboards -- 4.2 Coverage Dashboards -- 4.3 Connecting Coverage to the Verification Plan -- 4.4 Template Aware Coverage -- 5 Conclusions -- References -- Verification of Robotics -- Coverage-Driven Verification --- An Approach to Verify Code for Robots that Directly Interact with Humans -- 1 Introduction -- 2 Coverage-Driven Verification -- 2.1 Structure of a CDV Testbench -- 2.2 Test Generator -- 2.3 Driver -- 2.4 Checker -- 2.5 Coverage Collector -- 2.6 CDV Methodology -- 3 CDV Implementation -- 3.1 Case Study: Robot to Human Object Handover Task -- 3.2 Requirements -- 3.3 CDV Testbench Implementation -- 3.4 Test Generator and Driver -- 3.5 Checker -- 3.6 Coverage Collector -- 4 Experiments and Verification Results -- 5 Conclusions -- References -- Symbolic Execution -- PANDA: Simultaneous Predicate Abstraction and Concrete Execution -- 1 Introduction -- 2 Preliminaries -- 3 PANDA Algorithm -- 3.1 Dynamic Pruning and Discovery of Feasible Covering Paths -- 3.2 Soundness and Termination -- 4 Implementation -- 5 Evaluation -- 6 Related Work -- 7 Conclusion -- References -- TSO to SC via Symbolic Execution -- 1 Introduction -- 2 Weak Memory Reorderings -- 3 Processes and Their Parallel Composition -- 4 Symbolic Store-Buffer Graphs -- 5 SC Program Generation -- 6 Experimental Results -- 7 Related Work -- 8 Conclusion -- References. 327 $aParallel Symbolic Execution: Merging In-Flight Requests -- 1 Introduction -- 2 Multi-threaded Symbolic Execution -- 2.1 Symbolic Execution -- 2.2 Single-Threaded Symbolic Execution -- 2.3 Going Multi-Threaded -- 3 Reducing Overall Solver Costs -- 3.1 Batching Solver Requests -- 3.2 Merging and Solving Requests -- 3.3 Merging vs. Caching -- 4 Implementation -- 5 Evaluation -- 5.1 Time Spent by the Solver -- 5.2 Thread-Based Parallel Symbolic Execution -- 5.3 Batching and Merging Parallel Requests -- 5.4 Prototype Limitations -- 5.5 Threats to Validity -- 6 Related Work -- 7 Conclusion -- References -- Model Checking -- Limited Mobility, Eventual Stability -- 1 Introduction -- 1.1 Related Work on Verifying Mobile IP -- 2 The Formal Framework -- 2.1 Just Discrete Systems -- 2.2 Finitary Abstraction -- 2.3 Partial System Abstraction -- 3 Modelling Mobility -- 3.1 IPv6 Mobility Basics -- 3.2 The System -- 3.3 Properties -- 4 Formal Verification of the System -- 4.1 Proving Eventual Stable Routing -- 4.2 Method I: From Stability to Safety -- 4.3 Method II -- 5 Conclusions -- References -- A New Refinement Strategy for CEGAR-Based Industrial Model Checking -- 1 Introduction -- 2 Preliminaries -- 3 Lazy Abstraction -- 4 Abstraction Refinement -- 4.1 Path Projection -- 5 Implementation and Experimental Results -- 6 Conclusion -- References -- Timed Systems -- Quasi-equal Clock Reduction: Eliminating Assumptions on Networks -- 1 Introduction -- 2 Preliminaries -- 3 Reducing Clocks in Networks of Timed Automata -- 3.1 Algorithm for Transformation of Networks -- 3.2 Transformation of Properties -- 4 Weak Bisimulation -- 5 Experimental Results -- References -- Resource-Parameterized Timing Analysis of Real-Time Systems -- 1 Introduction -- 2 Backgrounds -- 2.1 Related Work -- 3 Resource-Parameterized Timing Analysis -- 3.1 Response Time of Applications. 327 $a3.2 Behavior Models of PIM and PSM -- 4 Case Study: Turn Indication Systems -- 4.1 PIM Analysis -- 4.2 PSM Analysis -- 5 Conclusions -- References -- SAT Solving -- SAT-Based Explicit LTL Reasoning -- 1 Introduction -- 2 Preliminaries -- 3 Explicit LTL Reasoning -- 3.1 Temporal Transition System -- 3.2 System Construction -- 3.3 Related Work -- 4 LTL Satisfiability Checking -- 4.1 The Main Algorithm -- 4.2 Heuristics for State Elimination -- 5 Experiments on LTL Satisfiability Checking -- 5.1 Experimental Methodologies -- 5.2 Results -- 6 Concluding Remarks -- References -- Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers -- 1 Introduction -- 2 Background -- 3 Contribution I and II: Community-Focused Search, Bridge Variables, and VSIDS -- 4 Contribution III: Experimental Evidence Supporting Strong Correlation Between TGC and VSIDS -- 5 Contribution IV: Exponential Moving Average and Multiplicative Decay -- 6 Contribution V: A Faster Branching Heuristic Based on Adaptive Moving Average -- 7 Interpretation of Results -- 8 Related Work -- 9 Conclusions and Future Work -- References -- Multi Domain Verification -- Multi-Domain Verification of Power, Clock and Reset Domains -- Abstract -- 1 Introduction -- 2 Individual Domain Verification -- 2.1 Clock Domain Crossing -- 2.2 Reset Domain Crossing -- 2.3 Power Domain Crossing -- 3 Multi-Domain Verification -- 3.1 Domain Structure Verification -- 3.2 Domain Control Verification -- 3.3 Domain Crossing Verification -- 4 Results -- 5 Conclusion -- References -- Synthesis -- FudgeFactor: Syntax-Guided Synthesis for Accurate RTL Error Localization and Correction -- 1 Introduction -- 2 Related Work -- 3 ``Fudging'' Buggy RTL Circuits -- 3.1 Common Error Library -- 3.2 Error Modeling -- 3.3 Instrumentation of the Buggy Circuit -- 3.4 The 2QBF Problem -- 3.5 Miter Construction. 327 $a4 Selecting Areas for ``Fudging'' -- 4.1 SAT-Based Debugger -- 5 Experimental Methodology -- 6 Experimental Results -- 7 Conclusions -- References -- On Switching Aware Synthesis for Combinational Circuits -- 1 Introduction -- 2 Problem Statement -- 3 Input Pairing for and Gates -- 4 Evaluation: Synthetic Boolean Models -- 5 Evaluation: A Mini Instruction Decoder -- 6 Discussion -- References -- Author Index. 330 $aThis book constitutes the refereed proceedings of the 11th International Haifa Verification Conference, HVC 2015, held in Haifa, Israel, in November 2015. The 17 revised full papers and 4 invited talks presented were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on hybrid systems; tools; verification of robotics; symbolic execution; model checking; timed systems; SAT solving; multi domain verification; and synthesis. 410 0$aProgramming and Software Engineering,$x2945-9168 ;$v9434 606 $aSoftware engineering 606 $aComputer science 606 $aCompilers (Computer programs) 606 $aMachine theory 606 $aArtificial intelligence 606 $aComputer networks 606 $aSoftware Engineering 606 $aComputer Science Logic and Foundations of Programming 606 $aCompilers and Interpreters 606 $aFormal Languages and Automata Theory 606 $aArtificial Intelligence 606 $aComputer Communication Networks 615 0$aSoftware engineering. 615 0$aComputer science. 615 0$aCompilers (Computer programs). 615 0$aMachine theory. 615 0$aArtificial intelligence. 615 0$aComputer networks. 615 14$aSoftware Engineering. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aCompilers and Interpreters. 615 24$aFormal Languages and Automata Theory. 615 24$aArtificial Intelligence. 615 24$aComputer Communication Networks. 676 $a005.1 702 $aPiterman$b Nir$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910484890903321 996 $aHardware and Software, Verification and Testing$9772242 997 $aUNINA