The Resource Computer Aided Verification : 24th International conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 : proceedings, P. Madhusudan, Sanjit A. Seshia (eds.), (electronic resource)

Computer Aided Verification : 24th International conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 : proceedings, P. Madhusudan, Sanjit A. Seshia (eds.), (electronic resource)

Label
Computer Aided Verification : 24th International conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 : proceedings
Title
Computer Aided Verification
Title remainder
24th International conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 : proceedings
Statement of responsibility
P. Madhusudan, Sanjit A. Seshia (eds.)
Title variation
CAV 2012
Creator
Contributor
Subject
Genre
Language
eng
Member of
Cataloging source
GW5XE
Illustrations
illustrations
Index
index present
LC call number
QA76.76.V47
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2012
http://bibfra.me/vocab/lite/meetingName
CAV (Conference)
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorName
  • Madhusudan, P
  • Seshia, Sanjit A
Series statement
  • Lecture notes in computer science,
  • LNCS sublibrary. SL 1, Theoretical computer science and general issues
Series volume
7358
http://library.link/vocab/subjectName
Computer software
Label
Computer Aided Verification : 24th International conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 : proceedings, P. Madhusudan, Sanjit A. Seshia (eds.), (electronic resource)
Link
http://dx.doi.org/10.1007/978-3-642-31424-7
Instantiates
Publication
Antecedent source
unknown
Bibliography note
Includes bibliographical references and index
Color
multicolored
Contents
  • Formal Verification of Genetic Circuits
  • Chris J. Myers
  • From C to Infinity and Back: Unbounded Auto-active Verification with VCC
  • Michał Moskal
  • Deterministic Automata for the (F, G)-Fragment of LTL
  • Jan Křetínský and Javier Esparza
  • Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
  • Tomáš Brázdil, Krishnendu Chatterjee, Antonín Kučera and Petr Novotný
  • ACTL [inverted U] LTL Synthesis
  • Rüdiger Ehlers
  • Synthesis and Some of Its Challenges
  • Learning Boolean Functions Incrementally
  • Yu-Fang Chen and Bow-Yaw Wang
  • Interpolants as Classifiers
  • Rahul Sharma, Aditya V. Nori and Alex Aiken
  • Termination Analysis with Algorithmic Learning
  • Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi
  • Automated Termination Proofs for Java Programs with Cyclic Data
  • Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl
  • Proving Termination of Probabilistic Programs Using Patterns
  • Javier Esparza, Andreas Gaiser and Stefan Kiefer
  • Wolfgang Thomas
  • The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
  • Arnaud J. Venet
  • Diagnosing Abstraction Failure for Separation Logic-Based Analyses
  • Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph M. Wintersteiger --
  • Model Checking Cell Biology
  • David L. Dill
  • Synthesizing Programs with Constraint Solvers
  • Rastislav Bodik and Emina Torlak
  • IC3 and beyond: Incremental, Inductive Verification
  • Aaron R. Bradley
  • How to Prove Algorithms Linearisable
  • Gerhard Schellhorn, Heike Wehrheim and John Derrick
  • Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
  • Matthew Hague and Anthony Widjaja Lin
  • Software Model Checking via IC3
  • Alessandro Cimatti and Alberto Griggio
  • Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits
  • Călin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin
  • Assume-Guarantee Abstraction Refinement for Probabilistic Systems
  • Anvesh Komuravelli, Corina S. Păsăreanu and Edmund M. Clarke
  • A Method for Symbolic Computation of Abstract Operations
  • Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking
  • Cyrille Jegourel, Axel Legay and Sean Sedwards
  • Timed Relational Abstractions for Sampled Data Control Systems
  • Aditya Zutshi, Sriram Sankaranarayanan and Ashish Tiwari
  • Approximately Bisimilar Symbolic Models for Digital Control Systems
  • Rupak Majumdar and Majid Zamani
  • Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
  • Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya and Tiziana Rizzo, et al. --
  • Aditya Thakur and Thomas Reps
  • Leveraging Interpolant Strength in Model Checking
  • Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina
  • Detecting Fair Non-termination in Multithreaded Programs
  • Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal
  • Lock Removal for Concurrent Trace Programs
  • Vineet Kahlon and Chao Wang
  • Exercises in Nonstandard Static Analysis of Hybrid Systems
  • Ichiro Hasuo and Kohei Suenaga
  • A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
  • Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan and Andreas Podelski, et al.
  • An Axiomatic Memory Model for POWER Multiprocessors
  • Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian and Jade Alglave, et al.
  • nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces
  • Flavio M. De Paula, Alan J. Hu and Amir Nahir
  • Incremental, Inductive CTL Model Checking
  • Zyad Hassan, Aaron R. Bradley and Fabio Somenzi
  • Minimum Satisfying Assignments for SMT
  • Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
  • Matthew Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps and Phillip Porras, et al.
  • Automatic Quantification of Cache Side-Channels
  • Boris Köpf, Laurent Mauborgne and Martín Ochoa
  • Secure Programming via Visibly Pushdown Safety Games
  • William R. Harris, Somesh Jha and Thomas Reps --
  • Isil Dillig, Thomas Dillig, Kenneth L. McMillan and Alex Aiken
  • When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
  • Cheng-Shen Han and Jie-Hong Roland Jiang
  • A Solver for Reachability Modulo Theories
  • Akash Lal, Shaz Qadeer and Shuvendu K. Lahiri
  • On Decidability of Prebisimulation for Timed Automata
  • Shibashis Guha, Chinmay Narayan and S. Arun-Kumar
  • MGSyn: Automatic Synthesis for Industrial Automation
  • Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl and Alois Knoll
  • OpenNWA: A Nested-Word Automaton Library
  • Evan Driscoll, Aditya Thakur and Thomas Reps
  • Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification
  • Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik
  • SAFARI: SMT-Based Abstraction for Arrays with Interpolants
  • Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina
  • Bma: Visual Tool for Modeling and Analyzing Biological Networks
  • David Benque, Sam Bourton, Caitlin Cockerton, Byron Cook and Jasmin Fisher, et al.
  • Alternate and Learn: Finding Witnesses without Looking All over
  • APEX: An Analyzer for Open Probabilistic Programs
  • Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter and James Worrell
  • Recent Developments in FDR
  • Philip Armstrong, Michael Goldsmith, Gavin Lowe, Joël Ouaknine and Hristina Palikareva, et al. --
  • Nishant Sinha, Nimit Singhania, Satish Chandra and Manu Sridharan
  • A Complete Method for Symmetry Reduction in Safety Verification
  • Duc-Hiep Chu and Joxan Jaffar
  • Synthesizing Number Transformations from Input-Output Examples
  • Rishabh Singh and Sumit Gulwani
  • Acacia+, a Tool for LTL Synthesis
  • Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin and Jean-François Raskin
  • Ashish Tiwari
  • Euler: A System for Numerical Optimization of Programs
  • Swarat Chaudhuri and Armando Solar-Lezama
  • SPT: Storyboard Programming Tool
  • Rishabh Singh and Armando Solar-Lezama
  • CSolve: Verifying C with Liquid Types
  • Patrick Rondon, Alexander Bakst, Ming Kawaguchi and Ranjit Jhala
  • passert: A Tool for Debugging Parallel Programs
  • Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik
  • TRACER: A Symbolic Execution Tool for Verification
  • A Model Checker for Hierarchical Probabilistic Real-Time Systems
  • Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E. Santosa
  • Joogie: Infeasible Code Detection for Java
  • Stephan Arlt and Martin Schäf
  • Hector: An Equivalence Checker for a Higher-Order Fragment of ML
  • David Hopkins, Andrzej S. Murawski and C. -H. Luke Ong
  • Resource Aware ML
  • Jan Hoffmann, Klaus Aehlig and Martin Hofmann
  • Songzheng Song, Jun Sun, Yang Liu and Jin Song Dong
  • SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs
  • Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique Rebêlo
  • Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems
  • Tool Paper
  • Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout and Fatiha Zaïdi
  • HybridSAL Relational Abstracter
Dimensions
unknown
Extent
1 online resource (xvi, 789 p.)
File format
unknown
Form of item
online
Isbn
9783642314247
Isbn Type
(electronic bk.)
Level of compression
unknown
Other physical details
ill.
Quality assurance targets
not applicable
Reformatting quality
unknown
Sound
unknown sound
Specific material designation
remote
System control number
  • 4055492-01okla_normanlaw
  • (SIRSI)4055492
  • (Sirsi) o796988509
  • (OCoLC)796988509
Label
Computer Aided Verification : 24th International conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 : proceedings, P. Madhusudan, Sanjit A. Seshia (eds.), (electronic resource)
Link
http://dx.doi.org/10.1007/978-3-642-31424-7
Publication
Antecedent source
unknown
Bibliography note
Includes bibliographical references and index
Color
multicolored
Contents
  • Formal Verification of Genetic Circuits
  • Chris J. Myers
  • From C to Infinity and Back: Unbounded Auto-active Verification with VCC
  • Michał Moskal
  • Deterministic Automata for the (F, G)-Fragment of LTL
  • Jan Křetínský and Javier Esparza
  • Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
  • Tomáš Brázdil, Krishnendu Chatterjee, Antonín Kučera and Petr Novotný
  • ACTL [inverted U] LTL Synthesis
  • Rüdiger Ehlers
  • Synthesis and Some of Its Challenges
  • Learning Boolean Functions Incrementally
  • Yu-Fang Chen and Bow-Yaw Wang
  • Interpolants as Classifiers
  • Rahul Sharma, Aditya V. Nori and Alex Aiken
  • Termination Analysis with Algorithmic Learning
  • Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi
  • Automated Termination Proofs for Java Programs with Cyclic Data
  • Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl
  • Proving Termination of Probabilistic Programs Using Patterns
  • Javier Esparza, Andreas Gaiser and Stefan Kiefer
  • Wolfgang Thomas
  • The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
  • Arnaud J. Venet
  • Diagnosing Abstraction Failure for Separation Logic-Based Analyses
  • Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph M. Wintersteiger --
  • Model Checking Cell Biology
  • David L. Dill
  • Synthesizing Programs with Constraint Solvers
  • Rastislav Bodik and Emina Torlak
  • IC3 and beyond: Incremental, Inductive Verification
  • Aaron R. Bradley
  • How to Prove Algorithms Linearisable
  • Gerhard Schellhorn, Heike Wehrheim and John Derrick
  • Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
  • Matthew Hague and Anthony Widjaja Lin
  • Software Model Checking via IC3
  • Alessandro Cimatti and Alberto Griggio
  • Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits
  • Călin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin
  • Assume-Guarantee Abstraction Refinement for Probabilistic Systems
  • Anvesh Komuravelli, Corina S. Păsăreanu and Edmund M. Clarke
  • A Method for Symbolic Computation of Abstract Operations
  • Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking
  • Cyrille Jegourel, Axel Legay and Sean Sedwards
  • Timed Relational Abstractions for Sampled Data Control Systems
  • Aditya Zutshi, Sriram Sankaranarayanan and Ashish Tiwari
  • Approximately Bisimilar Symbolic Models for Digital Control Systems
  • Rupak Majumdar and Majid Zamani
  • Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
  • Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya and Tiziana Rizzo, et al. --
  • Aditya Thakur and Thomas Reps
  • Leveraging Interpolant Strength in Model Checking
  • Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina
  • Detecting Fair Non-termination in Multithreaded Programs
  • Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal
  • Lock Removal for Concurrent Trace Programs
  • Vineet Kahlon and Chao Wang
  • Exercises in Nonstandard Static Analysis of Hybrid Systems
  • Ichiro Hasuo and Kohei Suenaga
  • A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
  • Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan and Andreas Podelski, et al.
  • An Axiomatic Memory Model for POWER Multiprocessors
  • Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian and Jade Alglave, et al.
  • nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces
  • Flavio M. De Paula, Alan J. Hu and Amir Nahir
  • Incremental, Inductive CTL Model Checking
  • Zyad Hassan, Aaron R. Bradley and Fabio Somenzi
  • Minimum Satisfying Assignments for SMT
  • Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
  • Matthew Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps and Phillip Porras, et al.
  • Automatic Quantification of Cache Side-Channels
  • Boris Köpf, Laurent Mauborgne and Martín Ochoa
  • Secure Programming via Visibly Pushdown Safety Games
  • William R. Harris, Somesh Jha and Thomas Reps --
  • Isil Dillig, Thomas Dillig, Kenneth L. McMillan and Alex Aiken
  • When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
  • Cheng-Shen Han and Jie-Hong Roland Jiang
  • A Solver for Reachability Modulo Theories
  • Akash Lal, Shaz Qadeer and Shuvendu K. Lahiri
  • On Decidability of Prebisimulation for Timed Automata
  • Shibashis Guha, Chinmay Narayan and S. Arun-Kumar
  • MGSyn: Automatic Synthesis for Industrial Automation
  • Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl and Alois Knoll
  • OpenNWA: A Nested-Word Automaton Library
  • Evan Driscoll, Aditya Thakur and Thomas Reps
  • Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification
  • Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik
  • SAFARI: SMT-Based Abstraction for Arrays with Interpolants
  • Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina
  • Bma: Visual Tool for Modeling and Analyzing Biological Networks
  • David Benque, Sam Bourton, Caitlin Cockerton, Byron Cook and Jasmin Fisher, et al.
  • Alternate and Learn: Finding Witnesses without Looking All over
  • APEX: An Analyzer for Open Probabilistic Programs
  • Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter and James Worrell
  • Recent Developments in FDR
  • Philip Armstrong, Michael Goldsmith, Gavin Lowe, Joël Ouaknine and Hristina Palikareva, et al. --
  • Nishant Sinha, Nimit Singhania, Satish Chandra and Manu Sridharan
  • A Complete Method for Symmetry Reduction in Safety Verification
  • Duc-Hiep Chu and Joxan Jaffar
  • Synthesizing Number Transformations from Input-Output Examples
  • Rishabh Singh and Sumit Gulwani
  • Acacia+, a Tool for LTL Synthesis
  • Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin and Jean-François Raskin
  • Ashish Tiwari
  • Euler: A System for Numerical Optimization of Programs
  • Swarat Chaudhuri and Armando Solar-Lezama
  • SPT: Storyboard Programming Tool
  • Rishabh Singh and Armando Solar-Lezama
  • CSolve: Verifying C with Liquid Types
  • Patrick Rondon, Alexander Bakst, Ming Kawaguchi and Ranjit Jhala
  • passert: A Tool for Debugging Parallel Programs
  • Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik
  • TRACER: A Symbolic Execution Tool for Verification
  • A Model Checker for Hierarchical Probabilistic Real-Time Systems
  • Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E. Santosa
  • Joogie: Infeasible Code Detection for Java
  • Stephan Arlt and Martin Schäf
  • Hector: An Equivalence Checker for a Higher-Order Fragment of ML
  • David Hopkins, Andrzej S. Murawski and C. -H. Luke Ong
  • Resource Aware ML
  • Jan Hoffmann, Klaus Aehlig and Martin Hofmann
  • Songzheng Song, Jun Sun, Yang Liu and Jin Song Dong
  • SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs
  • Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique Rebêlo
  • Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems
  • Tool Paper
  • Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout and Fatiha Zaïdi
  • HybridSAL Relational Abstracter
Dimensions
unknown
Extent
1 online resource (xvi, 789 p.)
File format
unknown
Form of item
online
Isbn
9783642314247
Isbn Type
(electronic bk.)
Level of compression
unknown
Other physical details
ill.
Quality assurance targets
not applicable
Reformatting quality
unknown
Sound
unknown sound
Specific material designation
remote
System control number
  • 4055492-01okla_normanlaw
  • (SIRSI)4055492
  • (Sirsi) o796988509
  • (OCoLC)796988509

Library Locations

  • Architecture LibraryBorrow it
    Gould Hall 830 Van Vleet Oval Rm. 105, Norman, OK, 73019, US
    35.205706 -97.445050
  • Bizzell Memorial LibraryBorrow it
    401 W. Brooks St., Norman, OK, 73019, US
    35.207487 -97.447906
  • Boorstin CollectionBorrow it
    401 W. Brooks St., Norman, OK, 73019, US
    35.207487 -97.447906
  • Chinese Literature Translation ArchiveBorrow it
    401 W. Brooks St., RM 414, Norman, OK, 73019, US
    35.207487 -97.447906
  • Engineering LibraryBorrow it
    Felgar Hall 865 Asp Avenue, Rm. 222, Norman, OK, 73019, US
    35.205706 -97.445050
  • Fine Arts LibraryBorrow it
    Catlett Music Center 500 West Boyd Street, Rm. 20, Norman, OK, 73019, US
    35.210371 -97.448244
  • Harry W. Bass Business History CollectionBorrow it
    401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • History of Science CollectionsBorrow it
    401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • John and Mary Nichols Rare Books and Special CollectionsBorrow it
    401 W. Brooks St., Rm. 509NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • Library Service CenterBorrow it
    2601 Technology Place, Norman, OK, 73019, US
    35.185561 -97.398361
  • Price College Digital LibraryBorrow it
    Adams Hall 102 307 West Brooks St., Norman, OK, 73019, US
    35.210371 -97.448244
  • Western History CollectionsBorrow it
    Monnet Hall 630 Parrington Oval, Rm. 300, Norman, OK, 73019, US
    35.209584 -97.445414
Processing Feedback ...