Alur, Rajeev (ed.); Peled, Doron A. (ed.) 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] Cited in 1 ReviewCited in 1 Document 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 \textit{R. Alur} (ed.) and \textit{D. A. Peled} (ed.), Computer aided verification. 16th international conference, CAV 2004, Boston, MA, USA, July 13--17, 2004. Proceedings. Berlin: Springer (2004; Zbl 1056.68003) Full Text: DOI