zbMATH — the first resource for mathematics

Computer aided verification. 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005. Proceedings. (English) Zbl 1078.68004
Lecture Notes in Computer Science 3576. Berlin: Springer (ISBN 3-540-27231-3/pbk). xv, 564 p. (2005).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 1056.68003).
Indexed articles:
Necula, George C.; Gulwani, Sumit, Randomized algorithms for program analysis and verification, 1 [Zbl 1081.68628]
Bentley, Bob, Validating a modern microprocessor, 2-4 [Zbl 1081.68609]
Piazza, C.; Antoniotti, M.; Mysore, V.; Policriti, A.; Winkler, F.; Mishra, B., Algorithmic algebraic model checking. I: Challenges from systems biology, 5-19 [Zbl 1081.68056]
Barrett, Clark; Moura, Leonardo; Stump, Aaron, SMT-COMP: Satisfiability modulo theories competition, 20-23 [Zbl 1081.68607]
Lahiri, Shuvendu K.; Ball, Thomas; Cook, Byron, Predicate abstraction via symbolic decision procedures, 24-38 [Zbl 1081.68055]
Jhala, Ranjit; McMillan, K. L., Interpolant-based transition relation approximation, 39-51 [Zbl 1081.68622]
Păsăreanu, Corina S.; Pelánek, Radek; Visser, Willem, Concrete model checking with abstract matching and refinement, 52-66 [Zbl 1081.68631]
Ball, Thomas; Kupferman, Orna; Yorsh, Greta, Abstraction for falsification, 67-81 [Zbl 1081.68051]
Rabinovitz, Ishai; Grumberg, Orna, Bounded model checking of concurrent programs, 82-97 [Zbl 1081.68633]
Heljanko, Keijo; Junttila, Tommi; Latvala, Timo, Incremental and complete bounded model checking for full PLTL, 98-111 [Zbl 1081.68621]
Gupta, Anubhav; Strichman, Ofer, Abstraction refinement for bounded model checking, 112-124 [Zbl 1081.68620]
Tang, Daijue; Malik, Sharad; Gupta, Aarti; Ip, C. Norris, Symmetry reduction in SAT-based model checking, 125-138 [Zbl 1081.68636]
Xie, Yichen; Aiken, Alex, Saturn: A SAT-based tool for bug detection, 139-143 [Zbl 1081.68639]
Chander, Ajay; Espinosa, David; Islam, Nayeem; Lee, Peter; Necula, George, JVer: A Java verifier, 144-147 [Zbl 1081.68614]
Dwyer, Matthew B.; Hatcliff, John; Hoosier, Matthew; Robby, Matthew, Building your own software model checker using the Bogor extensible model checking framework, 148-152 [Zbl 1081.68617]
Barner, Sharon; Glazberg, Ziv; Rabinovitz, Ishai, Wolf – bug hunter for concurrent software using formal methods, 153-157 [Zbl 1081.68605]
Balakrishnan, G.; Reps, T.; Kidd, N.; Lal, A.; Lim, J.; Melski, D.; Gruian, R.; Yong, S.; Chen, C.-H.; Teitelbaum, T., Model checking x86 executables with CodeSurfer/x86 and WPDS++, 158-163 [Zbl 1081.68604]
Chaki, Sagar; Ivers, James; Sharygina, Natasha; Wallnau, Kurt, The ComFoRT reasoning framework, 164-169 [Zbl 1081.68613]
Kaivola, Roope, Formal verification of Pentium\(^\circledR\)4 components with symbolic simulation and inductive invariants, 170-184 [Zbl 1081.68624]
Arons, Tamarah; Elster, Elad; Fix, Limor; Mador-Haim, Sela; Mishaeli, Michael; Shalev, Jonathan; Singerman, Eli; Tiemeyer, Andreas; Vardi, Moshe Y.; Zuck, Lenore D., Formal verification of backward compatibility of microcode, 185-198 [Zbl 1081.68602]
Monniaux, David, Compositional analysis of floating-point linear numerical filters, 199-212 [Zbl 1081.93028]
Vecchié, Eric; de Simone, Robert, Syntax-driven reachable state space construction of synchronous reactive programs, 213-225 [Zbl 1081.68637]
Jobstmann, Barbara; Griesmayer, Andreas; Bloem, Roderick, Program repair as a game, 226-238 [Zbl 1081.68572]
Roy, Amitabha; Gopinath, K., Improved probabilistic models for 802.11 protocol verification, 239-252 [Zbl 1081.68526]
Younes, Håkan L. S., Probabilistic verification for “black-box” systems, 253-265 [Zbl 1081.68641]
Sen, Koushik; Viswanathan, Mahesh; Agha, Gul, On statistical model checking of stochastic systems, 266-280 [Zbl 1081.68635]
Armando, A.; Basin, D.; Boichut, Y.; Chevalier, Y.; Compagna, L.; Cuellar, J.; Hankes Drielsma, P.; Heám, P. C.; Kouchnarenko, O.; Mantovani, J.; Mödersheim, S.; von Oheimb, D.; Rusinowitch, M.; Santiago, J.; Turuani, M.; Viganò, L.; Vigneron, L., The AVISPA tool for the automated validation of internet security protocols and applications, 281-285 [Zbl 1081.68523]
Olivain, Julien; Goubault-Larrecq, Jean, The Orchids intrusion detection tool, 286-290 [Zbl 1081.68630]
Barrett, Clark; Fang, Yi; Goldberg, Benjamin; Hu, Ying; Pnueli, Amir; Zuck, Lenore, TVOC: A translation validator for optimizing compilers, 291-295 [Zbl 1081.68606]
Cook, Byron; Kroening, Daniel; Sharygina, Natasha, Cogent: Accurate theorem proving for program verification, 296-300 [Zbl 1081.68673]
Ivančić, F.; Yang, Z.; Ganai, M. K.; Gupta, A.; Shlyakhter, I.; Ashar, P., F-Soft: Software verification platform, 301-306 [Zbl 1081.68581]
Meir, Orly; Strichman, Ofer, Yet another decision procedure for equality logic, 307-320 [Zbl 1081.68627]
Nieuwenhuis, Robert; Oliveras, Albert, DPLL(\(T\)) with exhaustive theory propagation and its application to difference logic, 321-334 [Zbl 1081.68629]
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; van Rossum, Peter; Sebastiani, Roberto, Efficient satisfiability modulo theories via delayed theory combination, 335-349 [Zbl 1081.68610]
Sebastiani, Roberto; Tonetta, Stefano; Vardi, Moshe Y., Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking, 350-363 [Zbl 1081.68634]
d’Amorim, Marcelo; Roşu, Grigore, Efficient monitoring of \(\omega\)-languages, 364-378 [Zbl 1081.68050]
Benedikt, Michael; Bonifati, Angela; Flesca, Sergio; Vyas, Avinash, Verification of tree updates for optimization, 379-393 [Zbl 1081.68608]
Geeraerts, Gilles; Raskin, Jean-François; Van Begin, Laurent, Expand, enlarge and check …made efficient, 394-407 [Zbl 1081.68619]
Balaban, Ittai; Fang, Yi; Pnueli, Amir; Zuck, Lenore D., IIV: An invisible invariant verifier, 408-412 [Zbl 1081.68603]
Yavuz-Kahveci, Tuba; Bartzis, Constantinos; Bultan, Tevfik, Action Language Verifier, extended, 413-417 [Zbl 1081.68640]
Gardey, Guillaume; Lime, Didier; Magnin, Morgan; Roux, Olivier H., Romeo: A tool for analyzing time Petri nets, 418-423 [Zbl 1081.68618]
Pastor, Enric; Peña, Marco A.; Solé, Marc, TRANSYT: A tool for the verification of asynchronous concurrent systems, 424-428 [Zbl 1081.68632]
Younes, Håkan L. S., Ymer: A statistical model checker, 429-433 [Zbl 1081.68642]
Lal, Akash; Reps, Thomas; Balakrishnan, Gogul, Extended weighted pushdown systems, 434-448 [Zbl 1081.68625]
Conway, Christopher L.; Namjoshi, Kedar S.; Dams, Dennis; Edwards, Stephen A., Incremental algorithms for inter-procedural analysis of safety properties, 449-461 [Zbl 1081.68615]
Costan, A.; Gaubert, S.; Goubault, E.; Martel, M.; Putot, S., A policy iteration algorithm for computing fixed points in static analysis of programs, 462-475 [Zbl 1081.68616]
McPeak, Scott; Necula, George C., Data structure specifications via local equality axioms, 476-490 [Zbl 1081.68584]
Bradley, Aaron R.; Manna, Zohar; Sipma, Henny B., Linear ranking with reachability, 491-504 [Zbl 1081.68611]
Kahlon, Vineet; Ivančić, Franjo; Gupta, Aarti, Reasoning about threads communicating via locks, 505-518 [Zbl 1081.68623]
Loginov, Alexey; Reps, Thomas; Sagiv, Mooly, Abstraction refinement via inductive learning, 519-533 [Zbl 1081.68626]
Chaki, Sagar; Clarke, Edmund; Sinha, Nishant; Thati, Prasanna, Automated assume-guarantee reasoning for simulation conformance, 534-547 [Zbl 1081.68612]
Alur, Rajeev; Madhusudan, P.; Nam, Wonhong, Symbolic compositional verification by learning assumptions, 548-562 [Zbl 1081.68601]

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
Full Text: DOI