Uppaal: Status & developments (English)
Free access
- New search for: Larsen, Kim G.
- New search for: Pettersson, Paul
- New search for: Yi, Wang
- New search for: Larsen, Kim G.
- New search for: Pettersson, Paul
- New search for: Yi, Wang
In:
Computer Aided Verification
;
456-459
;
1997
- Article/Chapter (Book) / Electronic Resource
-
Title:Uppaal: Status & developments
-
Contributors:
-
Published in:Computer Aided Verification ; 456-459Lecture Notes in Computer Science ; 1254 ; 456-459
-
Publisher:
- New search for: Springer Berlin Heidelberg
-
Place of publication:Berlin, Heidelberg
-
Publication date:1997-01-01
-
Size:4 pages
-
ISBN:
-
ISSN:
-
DOI:
-
Type of media:Article/Chapter (Book)
-
Type of material:Electronic Resource
-
Language:English
-
Keywords:
-
Source:
Table of contents eBook
The tables of contents are generated automatically and are based on the data records of the individual contributions available in the index of the TIB portal. The display of the Tables of Contents may therefore be incomplete.
- 1
-
Practical challenges for industrial formal verification toolsMarschner, F. Erich et al. | 1997
- 3
-
Formal verification of digital systems, from ASICs to HW/SW codesign — a pragmatic approachHughes, Roger B. et al. | 1997
- 7
-
The industrial success of verification tools based on stålmarck's methodBorälv, Arne et al. | 1997
- 11
-
Formal verification — Applications & case studiesRowe, Martin et al. | 1997
- 12
-
Automatic abstraction techniques for propositional μ-calculus model checkingPardo, Abelardo / Hachtel, Gary D. et al. | 1997
- 24
-
A compositional rule for hardware design refinementMcMillan, K. L. et al. | 1997
- 36
-
Module checking revisitedKupferman, Orna / Vardi, Moshe Y. et al. | 1997
- 48
-
Using compositional preorders in the verification of sliding window protocolKaivola, Roope et al. | 1997
- 60
-
An efficient decision procedure for the theory of fixed-sized bit-vectorsCyrluk, David / Möller, Oliver / Rueß, Harald et al. | 1997
- 72
-
Construction of abstract state graphs with PVSGraf, Susanne / Saidi, Hassen et al. | 1997
- 84
-
Verification of a chemical process leak test procedureTurk, Adam L. / Probst, Scott T. / Powers, Gary J. et al. | 1997
- 95
-
Automatic datapath extraction for efficient usage of HDDKamhi, Gila / Weissberg, Osnat / Fix, Limor / Binyamini, Ziv / Shtadler, Ze'ev et al. | 1997
- 107
-
An n log n algorithm for online BDD refinementKlarlund, Nils et al. | 1997
- 119
-
Weak bisimulation for fully probabilistic processesBaier, Christel / Hermanns, Holger et al. | 1997
- 131
-
Towards a mechanization of cryptographic protocol verificationBolignano, Dominique et al. | 1997
- 143
-
Efficient model checking using tabled resolutionRamakrishna, Y. S. / Ramakrishnan, C. R. / Ramakrishnan, I. V. / Smolka, Scott A. / Swift, Terrance / Warren, David S. et al. | 1997
- 155
-
Containment of regular languages in non-regular timing diagram languages is decidableFisler, Kathi et al. | 1997
- 167
-
An improved reachability analysis method for strongly linear hybrid systems (extended abstract)Boigelot, Bernard / Bronne, Louis / Rassart, Stéphane et al. | 1997
- 179
-
Some progress in the symbolic verification of timed automataBozga, Marius / Maler, Oded / Pnueli, Amir / Yovine, Sergio et al. | 1997
- 191
-
STARI: A case study in compositional and hierarchical timing verificationTaşiran, Serdar / Brayton, Robert K. et al. | 1997
- 202
-
A provably correct embedded verifier for the certification of safety critical softwareCimatti, Alessandro / Giunchiglia, Fausto / Pecchiari, Paolo / Pietra, Bruno / Profeta, Joe / Romano, Dario / Traverso, Paolo / Yu, Bing et al. | 1997
- 214
-
Model checking in a microprocessor design projectBarrett, Geoff / McIsaac, Anthony et al. | 1997
- 226
-
Some thoughts on statecharts, 13 years laterHarel, David et al. | 1997
- 232
-
On-the-fly model checking under fairness that exploits symmetryGyuris, Viktor / Sistla, A. Prasad et al. | 1997
- 244
-
Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluationPandey, Manish / Bryant, Randal E. et al. | 1997
- 256
-
Parallelizing the Murϕ verifierStern, Ulrich / Dill, David L. et al. | 1997
- 268
-
A new heuristic for bad cycle detection using BDDsHardin, R. H. / Kurshan, R. P. / Shukla, S. K. / Vardi, M. Y. et al. | 1997
- 279
-
Efficient detection of vacuity in ACTL formulasBeer, Ilan / Ben-David, Shoham / Eisner, Cindy / Rodeh, Yoav et al. | 1997
- 291
-
Model checking and transitive-closure logicImmerman, Neil / Vardi, Moshe Y. et al. | 1997
- 303
-
Boolean and 2-adic numbers based techniques for verifying synchronous designsBerry, Gerard et al. | 1997
- 304
-
Programs with quasi-stable channels are effectively recognizableCécé, Gérard / Finkel, Alain et al. | 1997
- 316
-
Combining constraint solving and symbolic model checking for a class of systems with non-linear constraintsChan, William / Anderson, Richard / Beame, Paul / Notkin, David et al. | 1997
- 328
-
Relaxed visibility enhances partial order reductionKokkarinen, Ilkka / Peled, Doron / Valmari, Antti et al. | 1997
- 340
-
Partial-order reduction in symbolic state space explorationAlur, R. / Brayton, R. K. / Henzinger, T. A. / Qadeer, S. / Rajamani, S. K. et al. | 1997
- 352
-
Deadlock checking using net unfoldingsMelzer, Stephan / Römer, Stefan et al. | 1997
- 364
-
Trace table based approach for pipelined microprocessor verificationSawada, Jun / Hunt, Warren A. Jr. et al. | 1997
- 376
-
On combining formal and informal verificationYuan, Jun / Shen, Jian / Abraham, Jacob / Aziz, Adnan et al. | 1997
- 388
-
Efficient modeling of memory arrays in symbolic simulationVelev, Miroslav / Bryant, Randal E. / Jain, Alok et al. | 1997
- 400
-
Symbolic model checking of infinite state systems using presburger arithmeticBultan, Tevfik / Gerber, Richard / Pugh, William et al. | 1997
- 412
-
Parametrized verification of linear networks using automata as invariantsSistla, A. Prasad et al. | 1997
- 424
-
Symbolic model checking with rich assertional languagesResten, Y. / Maler, O. / Marcus, M. / Pnueli, A. / Shahar, E. et al. | 1997
- 436
-
The invariant checker: Automated deductive verification of reactive systemsSaïdi, Hassen et al. | 1997
- 440
-
The PEP toolGrahlmann, Bernd et al. | 1997
- 444
-
TermiLog: A system for checking termination of queries to logic programsLindenstrauss, N. / Sagiv, Y. / Serebrenik, A. et al. | 1997
- 448
-
Mosel: A sound and efficient tool for M2L(Str)Kelb, Peter / Margaria, Tiziana / Mendier, Michael / Gsottberger, Claudia et al. | 1997
- 452
-
The verus tool: A quantitative approach to the formal verification of real-time systemsCampos, Sérgio / Clarke, Edmund / Minea, Marius et al. | 1997
- 456
-
Uppaal: Status & developmentsLarsen, Kim G. / Pettersson, Paul / Yi, Wang et al. | 1997
- 460
-
HyTech: A model checker for hybrid systemsHenzinger, Thomas A. / Ho, Pei-Hsin / Wong-Toi, Howard et al. | 1997
- 464
-
SMC: A symmetry based model checker for verification of liveness propertiesSistla, A. P. / Miliades, L. / Gyuris, V. et al. | 1997
- 468
-
μcke — Efficient μ-calculus model checkingBiere, Armin et al. | 1997
- 472
-
Prod 3.2 An advanced tool for efficient reachability analysisVarpaaniemi, Kimmo / Heljanko, Keijo / Lilius, Johan et al. | 1997
- 476
-
VeriSoft: A tool for the automatic analysis of concurrent reactive softwareGodefroid, Patrice et al. | 1997
- 480
-
RuleBase: Model checking at IBMBeer, I. / Ben-David, S. / Eisner, C. / Geist, D. / Gluhovsky, L. / Heyman, T. / Landver, A. / Paanah, P. / Rodeh, Y. / Ronin, G. et al. | 1997