×

zbMATH — the first resource for mathematics

Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3–7, 2007. Proceedings. (English) Zbl 1119.68005
Lecture Notes in Computer Science 4590. Berlin: Springer (ISBN 978-3-540-73367-6/pbk). xv, 562 p. (2007).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 1114.68002).
Indexed articles:
de Moura, Leonardo; Dutertre, Bruno; Shankar, Natarajan, A tutorial on satisfiability modulo theories, 20-36 [Zbl 1135.68563]
Sinha, Nishant; Clarke, Edmund, SAT-based compositional verification using lazy learning, 39-54 [Zbl 1135.68483]
Cohen, Ariel; Namjoshi, Kedar S., Local proofs for global safety properties, 55-67 [Zbl 1135.68470]
Maler, Oded; Nickovic, Dejan; Pnueli, Amir, On synthesizing controllers from bounded-response properties, 95-107 [Zbl 1135.68477]
de Alfaro, Luca; Faella, Marco, An accelerated algorithm for 3-color parity games with an application to timed games, 108-120 [Zbl 1135.68485]
Jonsson, Bengt; Saksena, Mayank, Systematic acceleration in regular model checking, 131-144 [Zbl 1135.68475]
Abdulla, Parosh Aziz; Delzanno, Giorgio; Rezine, Ahmed, Parameterized verification of infinite-state processes with global conditions, 145-157 [Zbl 1135.68461]
Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter W.; Wies, Thomas; Yang, Hongseok, Shape analysis for composite data structures, 178-192 [Zbl 1135.68372]
Jhala, Ranjit; McMillan, Kenneth L., Array abstractions from proofs, 193-206 [Zbl 1135.68474]
Bouajjani, Ahmed; Fratani, Séverine; Qadeer, Shaz, Context-bounded analysis of multithreaded programs with dynamic linked structures, 207-220 [Zbl 1135.68365]
Kahlon, Vineet; Yang, Yu; Sankaranarayanan, Sriram; Gupta, Aarti, Fast and accurate static data-race detection for concurrent programs, 226-239 [Zbl 1135.68368]
Chen, Feng; Roşu, Grigore, Parametric and sliced causality, 240-253 [Zbl 1135.68468]
Katoen, Joost-Pieter; Klink, Daniel; Leucker, Martin; Wolf, Verena, Three-valued abstraction for continuous-time Markov chains, 311-324 [Zbl 1135.68476]
de Alfaro, Luca; Roy, Pritam, Magnifying-lens abstraction for Markov decision processes, 325-338 [Zbl 1135.68486]
Matsliah, Arie; Strichman, Ofer, Underapproximation for model-checking based on random cryptographic constructions, 339-351 [Zbl 1135.68478]
Wang, Chao; Yang, Zijiang; Gupta, Aarti; Ivančić, Franjo, Using counterexamples for improving the precision of reachability computation with polyhedra, 352-365 [Zbl 1135.68370]
Babić, Domagoj; Hu, Alan J., Structural abstraction of software verification conditions, 366-378 [Zbl 1135.68463]
Gulwani, Sumit; Tiwari, Ashish, An abstract domain for analyzing heap-manipulating low-level software, 379-392 [Zbl 1135.68366]
Wahl, Thomas, Adaptive symmetry reduction, 393-405 [Zbl 1135.68484]
Kupferman, Orna; Piterman, Nir; Vardi, Moshe Y., From liveness to promptness, 406-419 [Zbl 1135.03336]
Gupta, Anubhav; McMillan, Kenneth L.; Fu, Zhaohui, Automated assumption generation for compositional verification, 420-432 [Zbl 1135.68473]
Segelken, Marc, Abstraction and counterexample-guided construction of \(\omega \)-automata for model checking of step-discrete linear hybrid models, 433-448 [Zbl 1135.68482]
Nahhal, Tarik; Dang, Thao, Test coverage for continuous and hybrid systems, 449-462 [Zbl 1135.68346]
Plaku, Erion; Kavraki, Lydia E.; Vardi, Moshe Y., Hybrid systems: From verification to falsification, 463-476 [Zbl 1135.68479]
Amit, Daphna; Rinetzky, Noam; Reps, Thomas; Sagiv, Mooly; Yahav, Eran, Comparison under abstraction for verifying linearizability, 477-490 [Zbl 1135.68462]
Ball, Thomas; Kupferman, Orna; Sagiv, Mooly, Leaping loops in the presence of abstraction, 491-503 [Zbl 1135.68465]
Beyer, Dirk; Henzinger, Thomas A.; Théoduloz, Grégory, Configurable software verification: Concretizing the convergence of model checking and program analysis, 504-518 [Zbl 1135.68466]
Ganesh, Vijay; Dill, David L., A decision procedure for bit-vectors and arrays, 519-531 [Zbl 1135.68472]
Cimatti, Alessandro; Roveri, Marco; Schuppan, Viktor; Tonetta, Stefano, Boolean abstraction for temporal logic satisfiability, 532-546 [Zbl 1135.68469]

MSC:
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68Q60 Specification and verification (program logics, model checking, etc.)
00B25 Proceedings of conferences of miscellaneous specific interest
PDF BibTeX XML Cite
Full Text: DOI