07691nam 22008055 450 99646636170331620200705005724.03-540-45657-010.1007/3-540-45657-0(CKB)1000000000211984(SSID)ssj0000697473(PQKBManifestationID)11467625(PQKBTitleCode)TC0000697473(PQKBWorkID)10691891(PQKB)10277031(DE-He213)978-3-540-45657-5(MiAaPQ)EBC3072795(PPN)155209191(EXLCZ)99100000000021198420121227d2002 u| 0engurnn|008mamaatxtccrComputer Aided Verification[electronic resource] 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27-31, 2002 Proceedings /edited by Ed Brinksma, Kim G. Larsen1st ed. 2002.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2002.1 online resource (X, 362 p.) Lecture Notes in Computer Science,0302-9743 ;2404Bibliographic Level Mode of Issuance: Monograph3-540-43997-8 Includes bibliographical references at the end of each chapters and index.Invited Talks -- Software Analysis and Model Checking -- The Quest for Efficient Boolean Satisfiability Solvers -- Invited Tutorials -- On Abstraction in Software Verification -- The Symbolic Approach to Hybrid Systems -- Infinite Games and Verification -- Symbolic Model Checking -- Symbolic Localization Reduction with Reconstruction Layering and Backtracking -- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions -- Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking -- Abstraction/Refinement and Model Checking -- Liveness with (0,1, ?)- Counter Abstraction -- Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking -- Automatic Abstraction Using Generalized Model Checking -- Compositional/Structural Verification -- Property Checking via Structural Analysis -- Conformance Checking for Models of Asynchronous Message Passing Software -- A Modular Checker for Multithreaded Programs -- Timing Analysis -- Automatic Derivation of Timing Constraints by Failure Analysis -- Deciding Separation Formulas with SAT -- Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling -- SAT Based Methods -- Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT -- Applying SAT Methods in Unbounded Symbolic Model Checking -- SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques -- Semi-formal Bounded Model Checking -- Symbolic Model Checking -- Algorithmic Verification of Invalidation-Based Protocols -- Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving -- Automated Unbounded Verification of Security Protocols -- Tool Presentations -- Exploiting Behavioral Hierarchy for Efficient Model Checking -- IF-2.0: A Validation Environment for Component-Based Real-Time Systems -- The AVISS Security Protocol Analysis Tool -- SPeeDI — A Verification Tool for Polygonal Hybrid Systems -- NuSMV 2: An OpenSource Tool for Symbolic Model Checking -- The d/dt Tool for Verification of Hybrid Systems -- Infinite Model Checking -- Model Checking Linear Properties of Prefix-Recognizable Systems -- Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking -- On Discrete Modeling and Model Checking for Nonlinear Analog Systems -- Compositional/Structural Verification -- Synchronous and Bidirectional Component Interfaces -- Interface Compatibility Checking for Software Modules -- Practical Methods for Proving Program Termination -- Extended Model Checking -- Evidence-Based Model Checking -- Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification -- Vacuum Cleaning CTL Formulae -- Tool Presentations -- CVC: A Cooperating Validity Checker -- ?Chek: A Multi-valued Model-Checker -- PathFinder: A Tool for Design Exploration -- Abstracting C with abC -- AMC: An Adaptive Model Checker -- Code Verification -- Temporal-Safety Proofs for Systems Code -- Regular Model Checking and Acceleration -- Extrapolating Tree Transformations -- Regular Tree Model Checking -- Compressing Transitions for Model Checking -- Model Reduction -- Canonical Prefixes of Petri Net Unfoldings -- State Space Reduction by Proving Confluence -- Fair Simulation Minimization.This volume contains the proceedings of the conference on Computer Aided V- i?cation (CAV 2002), held in Copenhagen, Denmark on July 27-31, 2002. CAV 2002 was the 14th in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical - sults to concrete applications, with an emphasis on practical veri?cation tools, including algorithms and techniques needed for their implementation. The c- ference has traditionally drawn contributions from researchers as well as prac- tioners in both academia and industry. This year we received 94 regular paper submissions out of which 35 were selected. Each submission received an average of 4 referee reviews. In addition, the CAV program contained 11 tool presentations selected from 16 submissions. For each tool presentation, a demo was given at the conference. The large number of tool submissions and presentations testi?es to the liveliness of the ?eld and its applied ?avor.Lecture Notes in Computer Science,0302-9743 ;2404ComputersComputer logicSoftware engineeringMathematical logicArtificial intelligenceSpecial purpose computersTheory of Computationhttps://scigraph.springernature.com/ontologies/product-market-codes/I16005Logics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XSoftware Engineeringhttps://scigraph.springernature.com/ontologies/product-market-codes/I14029Mathematical Logic and Formal Languageshttps://scigraph.springernature.com/ontologies/product-market-codes/I16048Artificial Intelligencehttps://scigraph.springernature.com/ontologies/product-market-codes/I21000Special Purpose and Application-Based Systemshttps://scigraph.springernature.com/ontologies/product-market-codes/I13030Computers.Computer logic.Software engineering.Mathematical logic.Artificial intelligence.Special purpose computers.Theory of Computation.Logics and Meanings of Programs.Software Engineering.Mathematical Logic and Formal Languages.Artificial Intelligence.Special Purpose and Application-Based Systems.005.1Brinksma Ededthttp://id.loc.gov/vocabulary/relators/edtLarsen Kim Gedthttp://id.loc.gov/vocabulary/relators/edtMiAaPQMiAaPQMiAaPQBOOK996466361703316Computer Aided Verification772228UNISA04904nam 2200721 450 991078057530332120230912130643.01-282-05645-X97866120564511-4426-7608-610.3138/9781442676084(CKB)2420000000004129(OCoLC)666921713(CaPaEBR)ebrary10230647(SSID)ssj0000299474(PQKBManifestationID)11205779(PQKBTitleCode)TC0000299474(PQKBWorkID)10241439(PQKB)10134032(CaBNvSL)thg00600788 (DE-B1597)464560(OCoLC)944178079(DE-B1597)9781442676084(Au-PeEL)EBL4671619(CaPaEBR)ebr11257324(VaAlCD)20.500.12592/h1x4zr(schport)gibson_crkn/2009-12-01/5/417468(MiAaPQ)EBC4671619(MdBmJHUP)musev2_104872(MiAaPQ)EBC3258446(EXLCZ)99242000000000412920160921e20011991 uy 0engurcn|||||||||txtccrIn the national interest a chronicle of the National Film Board of Canada from 1949 to 1989 /Gary EvansToronto, [Ontario] ;Buffalo, [New York] ;London, [England] :University of Toronto Press,2001.©19911 online resource (426 p.) HeritageIncludes index.0-8020-6833-2 Includes bibliographical references and index.Contents -- Preface -- Acknowledgments -- 1 Almost Derailed: Trying to Fit the National Film Board into the Postwar World -- 2 Down the Road from Ottawa to Montreal -- 3 The Golden Years -- 4 The Golden Years, Part II At the Heart of the Film Board: Unit B -- 5 Art for Whose Sake? -- 6 Clouds Gather above Centennial Glamour -- 7 Austerity -- 8 In Search of a Mission: Challenge for Change -- 9 'On a Chariot of Fire': Sydney Newman's Tenure -- 10 The Chariot Disintegrates and Burns. -- 11 Andre Lamy, Controlled by Events -- 12 The Atmosphere Changes from Siege to Neglect -- 13 Not with a Bang or a Whimper: Approaching a Second Half-century -- Afterword -- Appendices -- 1 Television films completed in fiscal year 1964-65 -- 2 Sponsored films made for various government departments and agencies, 1966-67 -- 3 Films of the Challenge for Change programme -- 4 Oscar awards and nominations through 1989 -- 5 Chronology of the best films of French Production to 1984. -- 6 Film commissioners and directors of English and French Production, Distribution, and Technical Operations7 Museum of Modern Art 50th anniversary sampler of Film Board films (May 1989) -- Notes -- Index.One of the cornerstones of Canadian culture, the National Film Board has throughout its history mirrored the social issues that preoccupy Canadians. Gary Evans traces the de- velopment of the postwar NFB, picking up the story where he left it at the end of his earlier work, John Grierson and the National Film Board: The Politics of Wartime Propaganda. Evans points out that although Ottawa has not meddled in the operation of the NFB, outside stimuli have regularly forced the Film Board to reassess its mandate, a process which often has brought about as much confusion as light. For example, the unbridled optimism and expansion of the fifties and sixties led to English Production's desire for 'democratization' of programming, an end to the power of executive producers, and an expansion of the Film Board's core of permanent employees, all of which nearly caused the organization to founder. On the French side, despite the filmmakers' preference for the feature film rather than the cinema verite documentary, many in Ottawa regarded their 'political' films as both unfair attacks on the federal system and anachronisms coming from a federal institution. Throughout, the English-French tug of war so integral to the Canadian identity is a recurring theme. Sources include interviews with former ministers, government film commissioners, policy-makers, and filmmakers, as well as archival documents and films. From them Evans has produced the first study to document the key trends in postwar Canadian filmmaking and to examine the role of film in the evolution of federal cultural policy.Motion picturesCanadaCanadafastLivres numeriques.History.e-books.Electronic books. Motion pictures354.7100854Evans Gary1944-1522677MiAaPQMiAaPQMiAaPQBOOK9910780575303321In the national interest3762515UNINA