×

Computer aided verification. 16th international conference, CAV 2004, Boston, MA, USA, July 13–17, 2004. Proceedings. (English) Zbl 1056.68003

Lecture Notes in Computer Science 3114. Berlin: Springer (ISBN 3-540-22342-8/pbk). xii, 536 p. (2004).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 1027.00031).
Indexed articles:
Rob Tristan Gerth: 1956-2003, 1-14 [Zbl 1103.01309]
Reps, Thomas W.; Sagiv, Mooly; Wilhelm, Reinhard, Static program analysis via 3-valued logic, 15-30 [Zbl 1103.68635]
Ray, Sandip; Hunt, Warren A. jun., Deductive verification of pipelined machines using first-order quantification, 31-43 [Zbl 1103.68634]
Gao, Hui; Hesselink, Wim H., A formal reduction for lock-free parallel algorithms, 44-56 [Zbl 1103.68980]
Namjoshi, Kedar S., An efficiently checkable, proof-based formulation of vacuity in model checking, 57-69 [Zbl 1103.68075]
Tiwari, Ashish, Termination of linear programs, 70-82 [Zbl 1103.68037]
Lange, Martin, Symbolic model checking of non-regular properties, 83-95 [Zbl 1103.68629]
Awedh, Mohammad; Somenzi, Fabio, Proving more properties with bounded model checking, 96-108 [Zbl 1103.68603]
Schröter, Claus; Khomenko, Victor, Parallel LTL-X model checking of high-level Petri nets based on unfoldings, 109-121 [Zbl 1103.68637]
Chang, Jacob; Berezin, Sergey; Dill, David L., Using interface refinement to integrate formal verification into the design cycle, 122-134 [Zbl 1103.68610]
Lahiri, Shuvendu K.; Bryant, Randal E., Indexed predicate discovery for unbounded system verification, 135-147 [Zbl 1103.68627]
Talupur, Muralidhar; Sinha, Nishant; Strichman, Ofer; Pnueli, Amir, Range allocation for separation logic, 148-161 [Zbl 1103.68079]
de Moura, Leonardo; Rueß, Harald, An experimental evaluation of ground decision procedures, 162-174 [Zbl 1103.68645]
Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare, DPLL(\(T\)): Fast decision procedures, 175-188 [Zbl 1103.68616]
Bustan, Doron; Rubin, Sasha; Vardi, Moshe Y., Verifying \(\omega\)-regular properties of Markov chains, 189-201 [Zbl 1103.68072]
Sen, Koushik; Viswanathan, Mahesh; Agha, Gul, Statistical model checking of black-box probabilistic systems, 202-215 [Zbl 1103.68639]
Yang, Jin; Seger, Carl-Johan H., Compositional specification and model checking in GSTE, 216-228 [Zbl 1103.68643]
Sebastiani, Roberto; Singerman, Eli; Tonetta, Stefano; Vardi, Moshe Y., GSTE is partitioned model checking, 229-241 [Zbl 1103.68638]
Fournet, Cédric; Hoare, Tony; Rajamani, Sriram K.; Rehof, Jakob, Stuck-free conformance, 242-254 [Zbl 1103.68612]
Goel, Amit; Bryant, Randal E., Symbolic simulation, model checking and abstraction with partially ordered Boolean functional vectors, 255-267 [Zbl 1103.68617]
Jiang, Jie-Hong R.; Brayton, Robert K., Functional dependency for verification reduction, 268-280 [Zbl 1103.68624]
Immerman, Niel; Rabinovich, Alexander; Reps, Thomas W.; Sagiv, Mooly; Yorsh, Great, Verification via structure simulation, 281-294 [Zbl 1103.68623]
Wang, Farn, Symbolic parametric safety analysis of linear hybrid systems with BDD-like data-structures, 295-307 [Zbl 1103.68642]
Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer, Abstraction-based satisfiability solving of Presburger arithmetic, 308-320 [Zbl 1103.68626]
Bartzis, Constantinos; Bultan, Tevfik, Widening arithmetic automata, 321-333 [Zbl 1103.68606]
Metzner, Alexander, Why model checking can improve WCET analysis, 334-347 [Zbl 1103.68631]
Abdulla, Parosh Aziz; Jonsson, Bengt; Nilsson, Marcus; d’Orso, Julien; Saksena, Mayank, Regular model checking for LTL(MSO), 348-360 [Zbl 1103.68070]
Finkel, Alain; Leroux, Jérôme, Image computation in infinite state model checking, 361-371 [Zbl 1103.68073]
Bouajjani, Ahmed; Habermehl, Peter; Vojnar, Tomáš, Abstract regular model checking, 372-386 [Zbl 1103.68071]
Piterman, Nir; Vardi, Moshe Y., Global model-checking of infinite-state systems, 387-400 [Zbl 1103.68077]
Gopalakrishnan, Ganesh; Yang, Yue; Sivaraj, Hemanthkumar, QB or not QB: An efficient execution verification tool for memory orderings, 401-413 [Zbl 1103.68618]
Arons, Tamarah, Verification of an advanced Mips-type out-of-order execution algorithm, 414-426 [Zbl 1103.68601]
Bingham, Jesse; Condon, Anne; Hu, Alan J.; Qadeer, Shaz; Zhang, Zhichuan, Automatic verification of sequential consistency for unbounded addresses and data values, 427-439 [Zbl 1103.68607]
Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav, Efficient modeling of embedded memories in bounded model checking, 440-452 [Zbl 1103.68615]
Groce, Alex; Kroening, Daniel; Lerda, Flavio, Understanding counterexamples with explain, 453-456 [Zbl 1103.68620]
Ball, Thomas; Cook, Byron; Lahiri, Shuvendu K.; Zhang, Lintao, Zapato: Automatic theorem proving for predicate abstraction refinement, 457-461 [Zbl 1103.68604]
Artho, Cyrille; Schuppan, Viktor; Biere, Armin; Eugster, Pascal; Baur, Marcel; Zweimüller, Boris, JNuke: Efficient dynamic analysis for Java, 462-465 [Zbl 1103.68602]
Pingree, Paula J.; Mikk, Erich, The HiVy tool set, 466-469 [Zbl 1103.68632]
Braberman, Víctor; Garbervetsky, Diego; Olivero, Alfredo, ObsSlice: A timed automata slicer based on observers, 470-474 [Zbl 1103.68608]
Lahiri, Shuvendu K.; Seshia, Sanjit A., The UCLID decision procedure, 475-478 [Zbl 1103.68628]
Gammie, Peter; van der Meyden, Ron, MCK: Model checking the logic of knowledge, 479-483 [Zbl 1103.68614]
Andrews, Tony; Qadeer, Shaz; Rajamani, Sriram K.; Rehof, Jakob; Xie, Yichen, Zing: A model checker for concurrent software, 484-487 [Zbl 1103.68600]
Griffault, Alain; Vincent, Aymeric, The Mec 5 model-checker, 488-491 [Zbl 1103.68619]
Tan, Li, PlayGame: A platform for diagnostic games, 492-495 [Zbl 1103.68641]
de Moura, Leonardo; Owre, Sam; Rueß, Harald; Rushby, John; Shankar, N.; Sorea, Maria; Tiwari, Ashish, SAL 2, 496-500 [Zbl 1103.68644]
Farzan, Azadeh; Chen, Feng; Meseguer, José; Roşu, Grigore, Formal analysis of Java programs in JavaFAN, 501-505 [Zbl 1103.68611]
Ramesh, S.; Sonalkar, Sampada; D’silva, Vijay; Chandra, Naveen; Vijayalakshmi, B., A toolset for modelling and verification of GALS systems, 506-509 [Zbl 1103.68633]
Fu, Xiang; Bultan, Tevfik; Su, Jianwen, WSAT: A tool for formal analysis of web services, 510-514 [Zbl 1103.68613]
Barrett, Clark; Berezin, Sergey, CVC Lite: A new implementation of the cooperating validity checker – Category B, 515-518 [Zbl 1103.68605]
Jin, HoonSang; Awedh, Mohammad; Somenzi, Fabio, CirCUs: A satisfiability solver geared towards bounded model checking, 519-522 [Zbl 1103.68625]
Hunt, Warren A. jun., Mechanical mathematical methods for microprocessor verification, 523-533 [Zbl 1103.68622]

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

Citations:

Zbl 1027.00031

Software:

SLAM; Bandera
PDFBibTeX XMLCite
Full Text: DOI