Updated on Fri Aug 27 18:27:57 2010

[Althaus et al., 2010]
Ernst Althaus, Sebastian Altmeyer, and Rouven Naujoks. A new combinatorial approach to parametric path analysis. AVACS Technical Report No.  58, SFB/TR 14 AVACS, June 2010. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Calin et al., 2010]
Georgel Calin, Pepijn Crouzen, Ernst Moritz Hahn, Pedro D'Argenio, and Lijun Zhang. Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. AVACS Technical Report No.  64, SFB/TR 14 AVACS, June 2010. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Christ and Hoenicke, 2010]
Jürgen Christ and Jochen Hoenicke. Instantiation-based interpolation for quantified formulae. In SMT 2010: 8th International Workshop on Satisfiability Modulo Theories, 2010.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Crouzen et al., 2010]
Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns, Abhishek Dhama, Oliver Theel, Ralf Wimmer, Bettina Braitling, and Bernd Becker. Bounded fairness for probabilistic distributed algorithms. AVACS Technical Report No.  57, SFB/TR 14 AVACS, April 2010. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Damm et al., 2010]
Werner Damm, Henning Dierks, Jens Oehlerking, and Amir Pnueli. Towards component based design of hybrid systems: Safety and stability. In Time for Verification: Essays in Meory of Amir Pnueli, number 6200 in Lecture Notes in Computer Science, 2010.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Dhama and Theel, 2010]
Abhishek Dhama and Oliver Theel. A transformational approach for designing scheduler-oblivious self-stabilizing algorithms. In 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2010), Lecture Notes in Computer Science, page To Appear. Springer, 2010.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Dräger et al., 2010]
Klaus Dräger, Andrey Kupriyanov, Bernd Finkbeiner, and Heike Wehrheim. Slab: A certifying model checker for infinite-state concurrent systems. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science. Springer-Verlag, 2010.
Abstract (click to open/close)

Subproject(s): R1,S1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Ehlers, 2010a]
Rüdiger Ehlers. Minimising deterministic büchi automata precisely using sat solving. In O. Strichman and S. Szeider, editors, 13th Thirteenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), volume 6175 of LNCS, pages 326-332. Springer Verlag, 2010.
Abstract (click to open/close)


Bibtex
© Springer Verlag (see article at SpringerLink)

[Ehlers, 2010b]
Rüdiger Ehlers. Short witnesses and accepting lassos in omega -automata. In 4th International Conference on Language and Automata Theory and Applications (LATA 2010), pages 261-272. Springer Verlag, 2010.
Abstract (click to open/close)

Subproject(s): S1

Bibtex
© Springer Verlag (see article at SpringerLink)

[Ehlers, 2010c]
Rüdiger Ehlers. Symbolic bounded synthesis. In T. Touili, B. Cook, and P. Jackson, editors, 22nd International Conference on Computer Aided Verification, volume 6174 of LNCS, pages 365-379. Springer Verlag, 2010.
Abstract (click to open/close)

Subproject(s): S1

Bibtex
© Springer Verlag (see article at SpringerLink)

[Eisentraut et al., 2010]
Christian Eisentraut, Holger Hermanns, and Lijun Zhang. On probabilistic automata in continuous time. AVACS Technical Report No.  62, SFB/TR 14 AVACS, August 2010. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Faber, 2010]
Johannes Faber. Verification Architectures: Compositional reasoning for real-time systems. AVACS Technical Report No.  65, SFB/TR 14 AVACS, August 2010. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Fränzle et al., 2010]
Martin Fränzle, Tino Teige, and Andreas Eggers. Satisfaction meets expectations: Computing expected values of probabilistic hybrid systems with smt. In Dominique Méry and Stephan Merz, editors, Integrated Formal Methods 2010, Lecture Notes in Computer Science. Springer, 2010.
Abstract (click to open/close)

Subproject(s): H1/2,H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Hahn et al., 2010]
Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. PASS: Abstraction refinement for infinite probabilistic models. In TACAS. Springer, 2010.
Abstract (click to open/close)

Subproject(s): S2,S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Heizmann et al., 2010]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Nested interpolants. In POPL, pages 471-482, 2010.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Hoenicke et al., 2010]
J. Hoenicke, E.-R. Olderog, and A. Podelski. Fairness for dynamic control. In J. Esparza and R. Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science. Springer-Verlag, 2010. To appear.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Ihlemann and Sofronie-Stokkermans, 2010a]
Carsten Ihlemann and Viorica Sofronie-Stokkermans. On hierarchical reasoning in combinations of theories. AVACS Technical Report No.  60, SFB/TR 14 AVACS, August 2010. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Ihlemann and Sofronie-Stokkermans, 2010b]
Carsten Ihlemann and Viorica Sofronie-Stokkermans. System description: H-pilot version 1.9. AVACS Technical Report No.  61, SFB/TR 14 AVACS, August 2010. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R1,H3

Bibtex

PDF
open

[Nopper et al., 2010]
Tobias Nopper, Christian Miller, Matthew Lewis, Bernd Becker, and Christoph Scholl. Sat modulo bdd - a combined verification approach for incomplete designs. In GI/ITG/GMM Workshop``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', 2010.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Olderog and Swaminathan, 2010]
Ernst-Rüdiger Olderog and Mani Swaminathan. Layered composition for timed automata. In Krishnendu Chatterjee and Thomas A. Henzinger, editors, The 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2010). Sringer Verlag, September 2010.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Podelski and Wies, 2010]
Andreas Podelski and Thomas Wies. Counterexample-guided focus. In 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 20-22, 2010. ACM, 2010.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Schlickling and Pister, 2010]
Marc Schlickling and Markus Pister. Semi-automatic derivation of timing models for WCET analysis. In LCTES '10: Proceedings of the 2010 ACM SIGPLAN-SIGBED conference on Languages, compilers, and tools for embedded systems. ACM, April 2010. To appear.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Teige and Fränzle, 2010]
Tino Teige and Martin Fränzle. Resolution for stochastic Boolean satisfiability. In Christian Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 17th International Conference (LPAR-17). Springer, 2010. to appear.
Abstract (click to open/close)

Subproject(s): H1/2,H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Toben et al., 2010]
Tobe Toben, Bernd Westphal, and Jan-Hendrik Rakow. Spotlight abstraction of agents and areas. In Bengt Jonsson, Jörg Kreiker, and Marta Kwiatkowska, editors, Quantitative and Qualitative Analysis of Network Protocols, number 10051 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2010. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany.
Abstract (click to open/close)

Keywords: Spotlight Abstraction, Verification, Dynamic Communication Systems
Subproject(s): S2

Bibtex

PDF
restricted

[Wachter and Zhang, 2010]
Björn Wachter and Lijun Zhang. Best probabilistic transformers. In VMCAI, pages 362-379, 2010.
Abstract (click to open/close)

Subproject(s): S2,S3

Bibtex

PDF
restricted

[Wimmer and Becker, 2010]
Ralf Wimmer and Bernd Becker. Correctness issues of symbolic bisimulation computation for Markov chains. In Bruno Müller-Clostermann, Klaus Echtle, and Erwin Rathgeb, editors, 15th International GI/ITG Conference on ``Measurement, Modelling and Evaluation of Computing Systems'', volume 5987 of Lecture Notes in Computer Science, pages 287-301, Essen, Germany, 2010. Springer-Verlag. (to appear).
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wimmer et al., 2010]
Ralf Wimmer, Salem Derisavi, and Holger Hermanns. Symbolic partition refinement with automatic balancing of time and space. Performance Evaluation, 67(9):815-835, 2010.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Zhang and Neuhäuser, 2010]
Lijun Zhang and Martin R. Neuhäuser. Model checking interactive markov chains. In Sixteenth International Conference on tools and algorithms for the construction and analysis of systems (TACAS), LNCS. Springer, 2010.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Ábrahám et al., 2009]
Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, and Christian Herde. Parallel SAT solving in bounded model checking. Journal of Logic and Computation, 2009.
Abstract (click to open/close)

Keywords: parallel programs, bounded model checking, SAT solving, linear programming, hybrid systems
Subproject(s): H1/2

Bibtex

PDF
restricted

[Althaus et al., 2009a]
Ernst Althaus, Evgeny Kruglov, and Christoph Weidenbach. Superposition modulo linear arithmetic sup(la). In Silvio Ghilardi and Roberto Sebastiani, editors, 7th international Symposium on Frontiers of Combining Systems (FroCos 2009), volume 5749 of Lecture Notes in Artificial Intelligence, pages 84-99, Trento, Italy, September 2009. Springer.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Althaus et al., 2009b]
Ernst Althaus, Evgeny Kruglov, and Christoph Weidenbach. Superposition modulo linear arithmetic sup(la). AVACS Technical Report No.  53, SFB/TR 14 AVACS, December 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open

[Altmeyer and Burguière, 2009]
Sebastian Altmeyer and Claire Burguière. A new notion of useful cache block to improve the bounds of cache- related preemption delay. In Proceedings of the 21st Euromicro Conference on Real-Time Systems (ECRTS '09), pages 109-118. IEEE Computer Society, July 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Altmeyer et al., 2009]
Sebastian Altmeyer, Claire Burguière, and Reinhard Wilhelm. Computing the maximum blocking time for scheduling with deferred preemption. In Workshop on Software Technologies for Future Dependable Distributed Systems, 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Badban et al., 2009a]
Bahareh Badban, Stefan Leue, and Jan-Georg Smaus. Automated invariant generation for the verification of real-time systems. In Andrew Ireland and Laura Kovacs, editors, Proceedings of the 2nd International Workshop on Invariant Generation, 2009.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open

[Badban et al., 2009b]
Bahareh Badban, Stefan Leue, and Jan-Georg Smaus. Automated predicate abstraction for real-time models. EPTCS, 10:36-43, 2009. Presented at INFINITY 2009, 11th International Workshop on Verification of Infinite-State Systems.
Subproject(s): R3

Bibtex

PDF
open

[Bercher and Mattmüller, 2009]
Pascal Bercher and Robert Mattmüller. Solving non-deterministic planning problems with pattern database heuristics. In Proceedings of the 32nd Annual Conference on Artificial Intelligence (KI 2009), pages 57-64, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Betz and Helmert, 2009]
Christoph Betz and Malte Helmert. Planning with h^+ in theory and practice. In Proceedings of the 32nd Annual German Conference on Artificial Intelligence (KI 2009), volume 5803 of LNAI, pages 9-16. Springer-Verlag, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Bode et al., 2009]
E. Bode, M. Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp, R. Pulungan, J. Rakow, R. Wimmer, and B. Becker. Compositional dependability evaluation for statemate. IEEE Transactions on Software Engineering, 35(2):274-292, 2009.
Abstract (click to open/close)

Keywords: checking, ctmc, mdp, model, stochastic

Bibtex

PDF
restricted

[Bogdoll et al., 2009]
Jonathan Bogdoll, Holger Hermanns, and Lijun Zhang. Flowsim simulation benchmarking platform. In Sixth International Conference on Quantitative Evaluation of Systems (QEST), pages 211-212. IEEE Computer Society, 2009.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Büker et al., 2009]
Matthias Büker, Alexander Metzner, and Ingo Stierand. Testing real-time task networks with functional extensions using model-checking. In 14th International Conference on Emerging Technologies and Factory Automation, 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Burguière et al., 2009]
Claire Burguière, Jan Reineke, and Sebastian Altmeyer. Cache-related preemption delay computation for set-associative caches--pitfalls and solutions. In Proceedings of 9th International Workshop on Worst-Case Execution Time (WCET) Analysis, June 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Cai et al., 2009]
Dunbo Cai, Jörg Hoffmann, and Malte Helmert. Enhancing the context-enhanced additive heuristic with precedence constraints. In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009), pages 50-57. AAAI Press, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Crouzen and Pulungan, 2009]
Pepijn Crouzen and Reza Pulungan. Acyclic phase-type distributions in fault trees. In Proceedings of the International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS), 2009.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Dhama et al., 2009]
Abhishek Dhama, Oliver Theel, Pepijn Crouzen, Holger Hermanns, Ralf Wimmer, and Bernd Becker. Dependability engineering of silent self-stabilizing systems. In Rachid Guerraoui and Franck Petit, editors, 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2009), volume Lecture Notes in Computer Science, page To Appear. Springer-Verlag, 2009.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Dierks et al., 2009]
Henning Dierks, Alexander Metzner, and Ingo Stierand. Efficient model-checking for real-time task networks. In 6th International Conference on Embedded Software and Systems, May 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Dimitrova and Finkbeiner, 2009]
Rayna Dimitrova and Bernd Finkbeiner. Synthesis of fault-tolerant distributed systems. In Zhiming Liu and Anders P. Ravn, editors, Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, volume 5799 of Lecture Notes in Computer Science, pages 321-336. Springer, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Dräger et al., 2009]
Klaus Dräger, Bernd Finkbeiner, , and Andreas Podelski. Directed model checking with distance-preserving abstractions. International Journal on Software Tools for Technology Transfer (STTT), 11(1):27-37, February 2009.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Dzetkuli v c and Ratschan, 2009]
Tomá v s Dzetkuli v c and Stefan Ratschan. How to capture hybrid systems evolution into slices of parallel hyperplanes. In ADHS'09: 3rd IFAC Conference on Analysis and Design of Hybrid Systems, pages 274-279, 2009.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
restricted

[Eggers et al., 2009a]
Andreas Eggers, Martin Fränzle, and Christian Herde. Application of constraint solving and ode-enclosure methods to the analysis of hybrid systems. In Theodore E. Simos, George Psihoyios, and Ch. Tsitouras, editors, NUMERICAL ANALYSIS AND APPLIED MATHEMATICS: International Conference on Numerical Analysis and Applied Mathematics 2009, volume 1168 of AIP Conference Proceedings, pages 1326-1330, Melville, New York, 2009. American Institue of Physics. copyright American Institute of Physics.
Abstract (click to open/close)

Keywords: hybrid discrete-continuous systems, verification, ordinary differential equations, constraint solving, PACS: 02.60.Lj, 02.70.-c, 89.75.-k
Subproject(s): H1/2

Bibtex

PDF
open

[Eggers et al., 2009b]
Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, and Tino Teige. Challenges in constraint-based analysis of hybrid systems. In Angelo Oddi, François Fages, and Francesca Rossi, editors, Recent Advances in Constraints -- 13th Annual ERCIM International Workshop on Constraint Solving and Constraint Logic Programming, CSCLP 2008, Rome, Italy, June 18-20, 2008, Revised Selected Papers, volume 5655 of Lecture Notes in Artificial Intelligence, pages 51-65, Berlin, Heidelberg, 2009. Springer. Springerlink: url http://www.springerlink.com/content/hx755817464v6746.
Abstract (click to open/close)

Keywords: mixed Boolean and arithmetic constraints - differential equations - stochastic SMT - Craig interpolation - parallel solver
Subproject(s): H1/2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Eisinger, 2009]
Jochen Eisinger. Automatenbasierte Entscheidungsverfahren für Theorien der Logik erster Stufe mit Addition. PhD thesis, Albert-Ludwigs-Universität Freiburg, Technische Fakultät, Institut für Informatik, Freiburg i. Br., 2009.
Subproject(s): H1/2

Bibtex

PDF
open

[Eyerich et al., 2009]
Patrick Eyerich, Robert Mattmüller, and Gabriele Röger. Using the context-enhanced additive heuristic for temporal and numeric planning. In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009), pages 130-137, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Faber, 2009]
J. Faber. Verification architectures for real-time systems. In M. Mousavi and E. Sekerinski, editors, Proceedings of Formal Methods 2009 Doctoral Symposium, number 09-15 in CS-Report, Eindhoven University of Technology, pages 14-19, 2009.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Finkbeiner and Kuhtz, 2009]
Bernd Finkbeiner and Lars Kuhtz. Monitor circuits for LTL with bounded and unbounded future. In Proceedings of the 9th International Workshop on Runtime Verification (RV 2009), LNCS. Springer, 2009.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Fränzle and Hansen, 2009]
Martin Fränzle and Michael R. Hansen. Efficient model checking for duration calculus. International Journal of Software and Informatics, 3(2-3):171-196, 2009.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Fränzle and Swaminathan, 2009]
Martin Fränzle and Mani Swaminathan. Revisiting decidability and optimum reachability for multi-priced timed automata. In J. Ouaknine and F. Vaandrager, editors, The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2009). Sringer Verlag, September 2009.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Fränzle et al., 2009]
Martin Fränzle, Andreas Eggers, Christian Herde, and Tino Teige. Hybrid discrete-continuous systems. In Modern Computational Science 09, pages 363-378. BIS-Verlag der Carl von Ossietzky Universität Oldenburg, 2009.
Subproject(s): H1/2

Bibtex

PDF
restricted

[Grund and Reineke, 2009]
Daniel Grund and Jan Reineke. Abstract interpretation of FIFO replacement. In Jens Palsberg and Zhendong Su, editors, Static Analysis, 16th International Symposium, SAS 2009, volume 5673 of LNCS, pages 120-136. Springer-Verlag, August 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Grund et al., 2009]
Daniel Grund, Jan Reineke, and Gernot Gebhard. Branch target buffers: WCET analysis and timing predictability. In 15th International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2009, August 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Haddad, 2009]
Walid Haddad. Verifying networks of phase event automata. Master thesis, Universität des Saarlandes, 2009.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Hahn et al., 2009a]
E. Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. Time-bounded model checking of infinite-state continuous-time markov chains. AVACS Technical Report No.  47, SFB/TR 14 AVACS, February 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Hahn et al., 2009b]
E. Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. Time-bounded model checking of infinite-state continuous-time markov chains. Fundamenta Informaticae, 95:129-155, 2009.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Hahn et al., 2009c]
Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. INFAMY: An infinite-state markov model checker. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, volume 5643 of LNCS, pages 641-647. Springer, 2009.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Hahn et al., 2009d]
Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric markov models. AVACS Technical Report No.  50, SFB/TR 14 AVACS, September 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Hahn et al., 2009e]
Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric markov models. In Corina S. Pasareanu, editor, Model Checking Software, 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings, volume 5578 of Lecture Notes in Computer Science, pages 88-106. Springer, 2009.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Hartmanns, 2009]
Arnd Hartmanns. A Modest checker for probabilistic timed automata. AVACS Technical Report No.  49, SFB/TR 14 AVACS, April 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Hartmanns and Hermanns, 2009]
Arnd Hartmanns and Holger Hermanns. A Modest approach to checking probabilistic timed automata. In Sixth International Conference on the Quantitative Evaluation of Systems (QEST), pages 187-196, Los Alamitos, CA, USA, 2009. IEEE Computer Society.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted

[Heise et al., 2009]
William Pihl Heise, Michael R. Hansen, and Martin Fränzle. A prototype of a model checker for duration calculus. In Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09, pages 26-28, Kgs. Lyngby, Denmark, 2009. DTU Informatics, Danmarks Tekniske Universitet.
Subproject(s): R1

Bibtex

[Heizmann et al., 2009]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Refinement of trace abstraction. In Jens Palsberg and Zhendong Su, editors, Static Analysis, 16th International Symposium, SAS 2009, volume 5673 of LNCS, pages 69-85. Springer-Verlag, August 2009.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Helmert, 2009]
Malte Helmert. Concise finite-domain representations for PDDL planning tasks. Artificial Intelligence, 173:503-535, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Helmert and Domshlak, 2009]
Malte Helmert and Carmel Domshlak. Landmarks, critical paths and abstractions: What's the difference anyway?. In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009), pages 162-169. AAAI Press, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Herbstritt, 2009]
Marc Herbstritt. Satisfiability & Verification: From Core Algorithms to Novel Application Domains. Suedwestdeutscher Verlag fuer Hochschulschriften (SVH), 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

[Hoffmann et al., 2009]
Jörg Hoffmann, Piergiorgio Bertoli, Malte Helmert, and Marco Pistore. Message-based web service composition, integrity constraints, and planning under uncertainty: A new connection. Journal of Artificial Intelligence Research, 35:49-117, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Horbach and Weidenbach, 2009a]
Matthias Horbach and Christoph Weidenbach. Decidability results for saturation-based model building. In Renate Schmidt, editor, 22nd International Conference on Automated Deduction (CADE-22), volume 5663 of Lecture Notes in Computer Science, pages 404-420, Montreal, Canada, 2009. Springer.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Horbach and Weidenbach, 2009b]
Matthias Horbach and Christoph Weidenbach. Deciding the inductive validity of for all there exists * queries. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, 23rd international Workshop, CSL 2009, volume 5771 of Lecture Notes in Computer Science, pages 332-347. Springer, 2009.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Ihlemann and Sofronie-Stokkermans, 2009]
Carsten Ihlemann and Viorica Sofronie-Stokkermans. System description: H-PILoT. In Automated Deduction - CADE-22. 22nd International Conference on Automated Deduction, number 5663 in LNAI. Springer, 2009.
Abstract (click to open/close)

Subproject(s): R1,H3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Jacobs, 2009]
Swen Jacobs. Incremental instance generation in local reasoning. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, CAV'09, volume 5643 of LNCS, pages 368-382. Springer, 2009.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Kalinnik et al., 2009]
Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, and Bernd Becker. Picoso -- A parallel interval constraint solver. In Hamid R. Arabnia, editor, Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA), Las Vegas, NV, USA, 2009. CSREA Press.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
restricted

[Katoen et al., 2009]
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, and David N. Jansen. The ins and outs of the probabilistic model checker MRMC. In Quantitative Evaluation of Systems (QEST), pages 167-176. IEEE Computer Society, 2009. url www.mrmc-tool.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Kuhtz and Finkbeiner, 2009]
Lars Kuhtz and Bernd Finkbeiner. LTL path checking is efficiently parallelizable. In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris Nikoletseas, and Wolfgang Thomas, editors, Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP 2009), Part II, volume 5556 of LNCS, pages 235-246. Springer, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Kupferschmid et al., 2009]
Stefan Kupferschmid, Tino Teige, Bernd Becker, and Martin Fränzle. Proofs of unsatisfiability for mixed boolean and non-linear arithmetic constraint formulae. In Carsten Gremzow and Nico Moser, editors, Proceedings of the 12th Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'' (MBMV 2009), pages 27-36. Universitätsverlag TU Berlin, 2009.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
restricted

[Maksoud et al., 2009]
Mohamed Abdel Maksoud, Markus Pister, and Marc Schlickling. An abstraction-aware compiler for VHDL models. In Proceedings of the International Conference on Computer Engineering and Systems (ICCES '09), pages 3-9. IEEE Computer Society, December 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Miller et al., 2009]
Christian Miller, Tobias Nopper, and Christoph Scholl. Symbolic CTL model checking for incomplete designs by selecting property-specific subsets of local component assumptions. In GI/ITG/GMM Workshop``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', March 2009.
Abstract (click to open/close)


Bibtex

PDF
restricted

[Müllner et al., 2009]
Nils Müllner, Abhishek Dhama, and Oliver Theel. Deriving a good trade-off between system availability and time redundancy. In Symposium on UbiCom Frontiers - Innovative Research Systems and Technologies. Carl von Ossietzky Universität Oldenburg, IEEE, July 2009.
Abstract (click to open/close)

Keywords: Availability, Self-Stabilization, Fault Tolerance, Prism, Simulation, SiSSDA, Limiting Window Availability
Subproject(s): S3

Bibtex

PDF
restricted

[Oehlerking and Theel, 2009a]
Jens Oehlerking and Oliver Theel. Decompositional construction of lyapunov functions for hybrid systems. In Rupak Majumdar and Paulo Tabuada, editors, 12th International Conference on Hybrid Systems: Computations and Control, Lecture Notes in Computer Science. Springer, 2009.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Oehlerking and Theel, 2009b]
Jens Oehlerking and Oliver Theel. A decompositional proof scheme for automated convergence proofs of stochastic hybrid systems. In Anders P. Ravn and Zhiming Liu, editors, 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), number 5799 in Lecture Notes in Computer Science. Springer, 2009. revised version.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Peter and Mattmüller, 2009]
Hans-Jörg Peter and Robert Mattmüller. Component-based abstraction refinement for timed controller synthesis. In Theodore Baker, editor, Proceedings of the 30th IEEE Real-Time Systems Symposium (RTSS 2009), December 1 - December 4, 2009, Washington, D.C., USA, pages 364-374, Los Alamitos, CA, USA, December 2009. IEEE Computer Society.
Abstract (click to open/close)

Subproject(s): R3,S1

Bibtex

PDF
open

[Pigorsch and Scholl, 2009]
Florian Pigorsch and Christoph Scholl. Exploiting structure in an AIG based QBF solver. In Conf. on Design, Automation and Test in Europe, pages 1596-1601, April 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Platzer and Quesel, 2009a]
André Platzer and Jan-David Quesel. European train control system: A case study in formal verification. AVACS Technical Report No.  54, SFB/TR 14 AVACS, October 2009. ISSN: 1860-9821, avacs.org.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
open

[Platzer and Quesel, 2009b]
André Platzer and Jan-David Quesel. European train control system: A case study in formal verification. In Ana Cavalcanti and Karin Breitman, editors, Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, December 9-12, 2009, Proceedings, volume 5885 of LNCS, pages 246-265, Heidelberg, 2009. Springer.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Platzer et al., 2009a]
André Platzer, Jan-David Quesel, and Philipp Rümmer. Real world verification. AVACS Technical Report No.  52, SFB/TR 14 AVACS, June 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
open

[Platzer et al., 2009b]
André Platzer, Jan-David Quesel, and Philipp Rümmer. Real world verification. In Renate A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2 - 7, 2009, Proceedings, volume 5663 of LNCS, pages 485-501. Springer, 2009.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Pulungan and Hermanns, 2009]
Reza Pulungan and Holger Hermanns. Acyclic minimality by construction--almost. In Fifth International Conference on the Quantitative Evaluation of Systems (QEST 2009), 13-16 September, 2009, Budapest, Hungary, pages 63-72. IEEE Computer Society, 2009.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Rabe and Schewe, 2009]
Markus Rabe and Sven Schewe. Optimal schedulers for time-bounded reachability in CTMDPs. AVACS Technical Report No.  55, SFB/TR 14 AVACS, October 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Ratschan and Smaus, 2009a]
Stefan Ratschan and Jan-Georg Smaus. Finding errors of hybrid systems by optimising an abstraction-based quality estimate. AVACS Technical Report No.  51, SFB/TR 14 AVACS, 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open

[Ratschan and Smaus, 2009b]
Stefan Ratschan and Jan-Georg Smaus. Finding errors of hybrid systems by optimising an abstraction-based quality estimate. In Catherine Dubois and Bertrand Meyer, editors, Proceedings of the 3rd International Conference on Tests And Proofs, volume 5668, pages 153-168, 2009.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open

[Richter and Helmert, 2009]
Silvia Richter and Malte Helmert. Preferred operators and deferred evaluation in satisficing planning. In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009), pages 273-280. AAAI Press, 2009.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Rybalchenko and Sofronie-Stokkermans, 2009]
Andrey Rybalchenko and Viorica Sofronie-Stokkermans. Constraint solving for interpolation. AVACS Technical Report No.  56, SFB/TR 14 AVACS, December 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Scholl et al., 2009]
C. Scholl, S. Disch, F. Pigorsch, and S. Kupferschmid. Computing optimized representations for non-convex polyhedra by detection and removal of redundant linear constraints. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 5505 of LNCS, pages 383-397. Springer, 2009.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Smaus and Hoffmann, 2009]
Jan-Georg Smaus and Jörg Hoffmann. Relaxation refinement: A new method to generate heuristic functions. In Doron Peled and Michael Wooldridge, editors, Proceedings of the 5th International Workshop on Model Checking and Artificial Intelligence (MOCHART 2008), volume 5348 of Lecture Notes in Artificial Intelligence, pages 146-164. Springer-Verlag, 2009.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Sofronie-Stokkermans, 2009a]
Viorica Sofronie-Stokkermans. Locality results for certain extensions of theories with bridging functions. In Automated Deduction - CADE-22. 22nd International Conference on Automated Deduction, number 5663 in LNAI. Springer, 2009.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Sofronie-Stokkermans, 2009b]
Viorica Sofronie-Stokkermans. Sheaves and geometric logic and applications to modular verification of complex systems. Electronic Notes in Theoretical Computer Science, 230:161-187, 2009.
Abstract (click to open/close)

Subproject(s): R1,H3

Bibtex

PDF
restricted

[Teige and Fränzle, 2009]
Tino Teige and Martin Fränzle. Constraint-based analysis of probabilistic hybrid systems. In A. Giua, C. Mahulea, M. Silva, and J. Zaytoon, editors, Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2009), pages 162-167. IFAC, 2009.
Abstract (click to open/close)

Keywords: Probabilistic hybrid systems, probabilistic logic, constraint satisfaction problems, problem solvers, automatic verification
Subproject(s): H1/2,H4

Bibtex

PDF
restricted

[Toben, 2009]
Tobe Toben. Analysis of Dynamic Evolution Systems by Spotlight Abstraction Refinement. PhD thesis, Carl von Ossietzky Universität Oldenburg, Germany, February 2009.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Wachter and Zhang, 2009]
Björn Wachter and Lijun Zhang. Best probabilistic transformers and beyond. AVACS Technical Report No.  48, SFB/TR 14 AVACS, April 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Wehrle and Helmert, 2009]
Martin Wehrle and Malte Helmert. The causal graph revisited for directed model checking. In Proceedings of the 16th International Static Analysis Symposium (SAS 2009), volume 5673 of LNCS, pages 86-101. Springer-Verlag, 2009.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Wehrle et al., 2009]
Martin Wehrle, Sebastian Kupferschmid, and Andreas Podelski. Transition-based directed model checking. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), volume 5505 of LNCS, pages 186-200. Springer-Verlag, 2009.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Wies, 2009]
Thomas Wies. Symbolic Shape Analysis. PhD thesis, University of Freiburg, 2009.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Wilhelm and Wachter, 2009]
Stephan Wilhelm and Björn Wachter. Symbolic state traversal for WCET analysis. In EMSOFT, pages 137-146, October 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Wilhelm et al., 2009]
Reinhard Wilhelm, Daniel Grund, Jan Reineke, Marc Schlickling, Markus Pister, and Christian Ferdinand. Memory hierarchies, pipelines, and buses for future architectures in time-critical embedded systems. IEEE Transactions on CAD of Integrated Circuits and Systems, 28(7):966-978, July 2009.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Wimmer et al., 2009]
Ralf Wimmer, Bettina Braitling, and Bernd Becker. Counterexample generation for discrete-time Markov chains using bounded model checking. In Neil D. Jones and Markus Müller-Olm, editors, Proceedings of the 10 textsuperscript th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), number 5403 in Lecture Notes in Computer Science, pages 366-380, Savannah, GA, USA, January 2009. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Altmeyer and Gebhard, 2008]
Sebastian Altmeyer and Gernot Gebhard. WCET analysis for preemptive systems. In Raimund Kirner, editor, Proceedings of the 8th International Workshop on Worst-Case Execution Time (WCET) Analysis, pages 105-112, Prague, Czech Republic, July 2008. OCG.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Altmeyer et al., 2008]
Sebastian Altmeyer, Christian Hümbert, Björn Lisper, and Reinhard Wilhelm. Parametric timing analyis for complex architectures. In Procedeedings of the 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'08), pages 367-376, Kaohsiung, Taiwan, August 2008. IEEE Computer Society.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Becker et al., 2008]
Bernd Becker, Marc Herbstritt, Natalia Kalinnik, Matthew Lewis, Juri Lichtner, Tobias Nopper, and Ralf Wimmer. Propositional approximations for bounded model checking of partial circuit designs. In Proceedings of the 26th IEEE International Conference on Computer Design, pages 52-59, Resort at Squaw Creek, Lake Tahoe, CA, USA, October 2008. IEEE Computer Society Press.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Bercher and Mattmüller, 2008]
Pascal Bercher and Robert Mattmüller. A planning graph heuristic for forward-chaining adversarial planning. In Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008), pages 921-922, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Böde et al., 2008a]
Eckard Böde, Thomas Peikenkamp, Jan Rakow, and Samuel Wischmeyer. Model based importance analysis for minimal cut sets. AVACS Technical Report No.  29, SFB/TR 14 AVACS, Apr 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Böde et al., 2008b]
Eckard Böde, Thomas Peikenkamp, Jan Rakow, and Samuel Wischmeyer. Model based importance analysis for minimal cut sets. In Automated Technology for Verification and Analysis, 6th International Symposium ATVA 2008, Seoul, Korea, volume 5311 of LNCS, pages 303-317, 2008.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Brückner et al., 2008]
Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Slicing abstractions. Fundamenta Informaticae, 89(4):369-392, 2008.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

[Crouzen et al., 2008]
Pepijn Crouzen, Holger Hermanns, and Lijun Zhang. No cycling? Go faster! On the minimization of acyclic models. AVACS Technical Report No.  41, SFB/TR 14 AVACS, September 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Dimitrova and Finkbeiner, 2008a]
Rayna Dimitrova and Bernd Finkbeiner. Abstraction refinement for games with incomplete information. AVACS Technical Report No.  43, SFB/TR 14 AVACS, November 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Dimitrova and Finkbeiner, 2008b]
Rayna Dimitrova and Bernd Finkbeiner. Abstraction refinement for games with incomplete information. In Ramesh Hariharan, Madhavan Mukund, and V. Vinay, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, December 9-11, 2008, Bangalore, India, volume 08004 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Dimitrova and Podelski, 2008]
Rayna Dimitrova and Andreas Podelski. Is lazy abstraction a decision procedure for broadcast protocols?. In Francesco Logozzo, Doron Peled, and Lenore D. Zuck, editors, Verification, Model Checking, and Abstract Interpretation, 9th International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008, Proceedings, volume 4905 of Lecture Notes in Computer Science, pages 98-111. Springer, 2008.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Dräger and Finkbeiner, 2008a]
Klaus Dräger and Bernd Finkbeiner. Subsequence invariants. AVACS Technical Report No.  42, SFB/TR 14 AVACS, June 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Dräger and Finkbeiner, 2008b]
Klaus Dräger and Bernd Finkbeiner. Subsequence invariants. In Franck van Breugel and Marsha Chechik, editors, Proceedings of the 19th International Conference on Concurrency Theory, volume 5201 of Lecture Notes in Computer Science, pages 172-168, Berlin Heidelberg, 2008. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): R1,R3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Eggers et al., 2008a]
A. Eggers, N. Kalinnik, S. Kupferschmid, and T. Teige. Challenges in constraint-based analysis of hybrid systems. In Proceedings of the Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming (CSCLP 2008), June 2008.
Abstract (click to open/close)

Subproject(s): H1/2,H4

Bibtex

PDF
open

[Eggers et al., 2008b]
Andreas Eggers, Martin Fränzle, and Christian Herde. SAT modulo ODE: A direct SAT approach to hybrid systems. AVACS Technical Report No.  37, SFB/TR 14 AVACS, April 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open

[Eggers et al., 2008c]
Andreas Eggers, Martin Fränzle, and Christian Herde. SAT modulo ODE: A direct SAT approach to hybrid systems. In Sungdeok (Steve) Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, and Mahesh Viswanathan, editors, Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08), volume 5311 of Lecture Notes in Computer Science, pages 171-185. Springer, 2008.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Eisinger, 2008]
Jochen Eisinger. Upper bounds on the automata size for integer and mixed real and integer linear arithmetic. In Proc. of the 17th EACSL Annual Conference on Computer Science Logic (CSL'08), Lecture Notes in Computer Science, pages 430-444, Berlin, Heidelberg, New York, 2008. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Eisinger and Klaedtke, 2008]
Jochen Eisinger and Felix Klaedtke. Don't care words with an application to the automata-based approach for real addition. Formal Methods in System Design, 33(1-3):85-115, 2008.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
restricted

[Finkbeiner et al., 2008a]
Bernd Finkbeiner, Hans-Jörg Peter, and Sven Schewe. RESY: Requirement synthesis for compositional model checking. In C.R. Ramakrishnan and Jakob Rehof, editors, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science, pages 463-466, Berlin Heidelberg, 2008. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Finkbeiner et al., 2008b]
Bernd Finkbeiner, Hans-Jörg Peter, and Sven Schewe. Synthesizing certificates in networks of timed automata. In Proceedings of the 29th IEEE Real-Time Systems Symposium (RTSS 2008), November 30 - December 3, 2008, Barcelona, Spain, pages 183-194, Los Alamitos, CA, USA, December 2008. IEEE Computer Society.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Fränzle, 2008]
Martin Fränzle. Engineering constraint solvers for the analysis of hybrid systems. In 20th Nordic Workshop on Programming Theory, NWPT '08, page 9. Institute of Cybernetics, Tallinn Technical University, 2008.
Subproject(s): H1/2,H4

Bibtex

[Fränzle and Hansen, 2008]
Martin Fränzle and Michael R. Hansen. Efficient model checking for duration calculus based on branching-time approximations. In Antonio Cerone and Stefan Gruner, editors, Proceedings of the 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM 08), pages 63-72. IEEE Computer Society Press, 2008.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Fränzle et al., 2008a]
M. Fränzle, H. Hermanns, and T. Teige. Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In Magnus Egerstedt and Bud Mishra, editors, Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC'08), volume 4981 of Lecture Notes in Computer Science, pages 172-186. Springer, 2008.
Abstract (click to open/close)

Subproject(s): H1/2,H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Fränzle et al., 2008b]
M. Fränzle, H. Hermanns, and T. Teige. Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In Pre-Proceedings of the ETAPS 2008 Sixth Workshop on Quantitative Aspects of Programming Languages (QAPL 2008), 2008. extended abstract.
Abstract (click to open/close)

Keywords: Stochastic satisfiability, infinite domains, probabilistic hybrid automata, probabilistic bounded reachability.
Subproject(s): H1/2,H4

Bibtex

PDF
open

[Grund and Reineke, 2008]
Daniel Grund and Jan Reineke. Estimating the performance of cache replacement policies. In MEMOCODE '08: Proceedings of the 6th IEEE/ACM International Conference on Formal Methods and Models for Codesign, pages 101-111, June 2008.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Helmert and Geffner, 2008]
Malte Helmert and Héctor Geffner. Unifying the causal graph and additive heuristics. In Proceedings of the 18th International Conference on Automated Planning and Scheduling (ICAPS 2008), pages 140-147. AAAI Press, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Helmert and Mattmüller, 2008]
Malte Helmert and Robert Mattmüller. Accuracy of admissible heuristic functions in selected planning domains. In Proceedings of the 23nd AAAI Conference on Artificial Intelligence (AAAI 2008), pages 938-943. AAAI Press, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Helmert and Röger, 2008]
Malte Helmert and Gabriele Röger. How good is almost perfect?. In Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI 2008), pages 944-949. AAAI Press, 2008.
Abstract (click to open/close)

Subproject(s): S1,R3

Bibtex

PDF
open

[Helmert et al., 2008]
Malte Helmert, Patrik Haslum, and Jörg Hoffmann. Explicit-state abstraction: A new method for generating heuristic functions. In Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI 2008), pages 1547-1550. AAAI Press, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Herde et al., 2008]
C. Herde, A. Eggers, M. Fränzle, and T. Teige. Analysis of hybrid systems using HySAT. In The Third International Conference on Systems (ICONS 2008), pages 196-201. IEEE Computer Society, 2008.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
restricted

[Hermanns et al., 2008]
Holger Hermanns, Björn Wachter, and Lijun Zhang. Probabilistic CEGAR. In Aarti Gupta and Sharad Malik, editors, Proceedings of the 20th Int'l Conf. on Computer Aided Verification, CAV 2008, volume 5123 of Lecture Notes in Computer Science, pages 162-175. Springer Verlag, 2008.
Abstract (click to open/close)

Subproject(s): S2, S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Horbach and Weidenbach, 2008]
Matthias Horbach and Christoph Weidenbach. Superposition for fixed domains. In Michael Kaminski and Simone Martini, editors, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, volume 5213 of LNCS, pages 293-307. Springer, 2008.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Ihlemann et al., 2008]
Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans. On local reasoning in verification. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 265-281. Springer, 2008.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Jacobs, 2008]
Swen Jacobs. Incremental instance generation in local reasoning. In Franz Baader, Silvio Ghilardi, Miki Hermann, Ulrike Sattler, and Viorica Sofronie-Stokkermans, editors, Complexity, Expressibility, and Decidability in Automated Reasoning, CEDAR'08, pages 47-62, 2008.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Kupferschmid et al., 2008a]
Sebastian Kupferschmid, Jörg Hoffmann, and Kim G. Larsen. Fast directed model checking via russian doll abstraction. In C. R. Ramakrishnan and Jakob Rehof, editors, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), volume 4963 of Lecture Notes in Computer Science, pages 203-217. Springer-Verlag, 2008.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Kupferschmid et al., 2008b]
Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, and Andreas Podelski. Faster than Uppaal?. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), volume 5123 of LNCS, pages 552-555. Springer-Verlag, 2008.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Kupferschmid et al., 2008c]
Stefan Kupferschmid, Tino Teige, Bernd Becker, and Martin Fränzle. Proofs of unsatisfiability for mixed boolean and non-linear arithmetic constraint formulae. AVACS Technical Report No.  40, SFB/TR 14 AVACS, June 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open

[Metzner, 2008]
Alexander Metzner. Scheduling of distributed real-time systems under functional constraints. In Proceedings of the 13th IEEE International Conference on Emerging Technologies and Factory Automation. IEEE Computer Society, 2008.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Meyer et al., 2008]
R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. Model checking duration calculus: A practical approach. Formal Aspects of Computing, 20(4-5):481-505, July 2008. ISSN 0934-5043 (Print) 1433-299X (Online).
Abstract (click to open/close)

Keywords: Model checking, Verification, Duration Calculus, Timed automata, Real-time systems, European Train Control System, Case study
Subproject(s): R1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Müllner et al., 2008]
Nils Müllner, Abhishek Dhama, and Oliver Theel. Derivation of fault tolerance measures of self-stabilizing algorithms by simulation. In ANSS '08: Proceedings of the 41st annual symposium on Simulation, Ottawa, ON, Canada, April 2008. IEEE Computer Society Press.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted

[Platzer, 2008a]
André Platzer. Differential-algebraic dynamic logic for differential-algebraic programs. Journal of Logic and Computation, 2008. Accepted for publication.
Abstract (click to open/close)

Keywords: dynamic logic, differential constraints, sequent calculus, verification of hybrid systems, differential induction, theorem proving
Subproject(s): H3

Bibtex

PDF
restricted

[Platzer, 2008b]
André Platzer. Differential dynamic logic for hybrid systems.. Journal of Automated Reasoning, 41(2):143-189, 2008. (c) Springer Verlag.
Abstract (click to open/close)

Keywords: dynamic logic, differential equations, sequent calculus, axiomatisation, automated theorem proving, verification of hybrid systems
Subproject(s): H3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Platzer and Clarke, 2008]
André Platzer and Edmund M. Clarke. Computing differential invariants of hybrid systems as fixedpoints. In Aarti Gupta and Sharad Malik, editors, Computer-Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pages 176-189. Springer, 2008.
Abstract (click to open/close)

Keywords: verification of hybrid systems, differential invariants, verification logic, fixedpoint engine
Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Platzer and Quesel, 2008a]
André Platzer and Jan-David Quesel. Keymaera: A hybrid theorem prover for hybrid systems. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, LNCS. Springer, 2008.
Abstract (click to open/close)

Keywords: dynamic logic, automated theorem proving, decision procedures, computer algebra, verification of hybrid systems
Subproject(s): H3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Platzer and Quesel, 2008b]
André Platzer and Jan-David Quesel. Logical verification and systematic parametric analysis in train control.. In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings, LNCS. Springer, 2008.
Abstract (click to open/close)

Keywords: parametric verification, logic for hybrid systems, symbolic decomposition
Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Pulungan and Hermanns, 2008]
Reza Pulungan and Holger Hermanns. Effective minimization of acyclic phase-type representations. AVACS Technical Report No.  38, SFB/TR 14 AVACS, March 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Ratschan and Smaus, 2008]
Stefan Ratschan and Jan-Georg Smaus. Finding errors of hybrid systems by optimising an abstraction-based quality estimate. In Tarmo Uustalu and Jüri Vain, editors, Proceedings of the 20th Nordic Workshop on Programming Theory, pages 72-74, 2008.
Subproject(s): H1/2

Bibtex

PDF
open

[Reineke and Grund, 2008a]
Jan Reineke and Daniel Grund. Relative competitive analysis of cache replacement policies. In LCTES, 2008. to appear.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Reineke and Grund, 2008b]
Jan Reineke and Daniel Grund. Relative competitiveness of cache replacement policies. In SIGMETRICS, 2008. to appear.
Subproject(s): R2

Bibtex

PDF
restricted

[Reineke and Grund, 2008c]
Jan Reineke and Daniel Grund. Sensitivity of cache replacement policies. AVACS Technical Report No.  36, SFB/TR 14 AVACS, March 2008. ISSN: 1860-9821, http://www.avacs.org; 1st reprint 2010.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Richter et al., 2008]
Silvia Richter, Malte Helmert, and Matthias Westphal. Landmarks revisited. In Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI 2008), pages 975-982. AAAI Press, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Röger et al., 2008]
Gabriele Röger, Malte Helmert, and Bernhard Nebel. On the relative expressiveness of ADL and Golog: The last piece in the puzzle. In Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning (KR 2008), pages 544-550. AAAI Press, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Schewe, 2008a]
Sven Schewe. ALT* satisfiability is 2EXPTIME-complete. AVACS Technical Report No.  35, SFB/TR 14 AVACS, February 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S1,S2

Bibtex

PDF
open

[Schewe, 2008b]
Sven Schewe. ATL* satisfiability is 2ExpTime-complete. In Proceedings of the 35th International Colloquium on Automata, Languages and Programming, Part II (ICALP 2008), 6-13 July, Reykjavik, Iceland, volume 5126 of Lecture Notes in Computer Science, pages 373-385. Springer-Verlag, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Schewe, 2008c]
Sven Schewe. An optimal strategy improvement algorithm for solving parity and payoff games. In Proceedings of the 17th Annual Conference of the European Association for Computer Science Logic (CSL 2008), 15-19 September, Bertinoro, Italy, volume 5213 of Lecture Notes in Computer Science, pages 368-383. Springer-Verlag, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Schewe, 2008d]
Sven Schewe. Synthesis of Distributed Systems. PhD thesis, Universität des Saarlandes, 2008.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Schmitt, 2008]
Christian Schmitt. Bounded model checking of probabilistic hybrid automata. Master's thesis, Carl von Ossietzky Universität Oldenburg, Department für Informatik, 2008.
Abstract (click to open/close)

Subproject(s): H1/2,H4

Bibtex

PDF
open

[Scholl et al., 2008]
Christoph Scholl, Stefan Disch, Florian Pigorsch, and Stefan Kupferschmid. Using an smt solver and craig interpolation to detect and remove redundant linear constraints in representations of non-convex polyhedra. In SMT '08/BPR '08: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, pages 18-26, New York, NY, USA, 2008. ACM.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted

[Sofronie-Stokkermans, 2008a]
Viorica Sofronie-Stokkermans. Efficient hierarchical reasoning about functions over numerical domains. AVACS Technical Report No.  45, SFB/TR 14 AVACS, December 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
open

[Sofronie-Stokkermans, 2008b]
Viorica Sofronie-Stokkermans. Efficient hierarchical reasoning about functions over numerical domains. In Andreas Dengel, Karsten Berns, Thomas M. Breuel, Frank Bomarius, and Thomas R. Roth-Berghofer, editors, KI 2008: Advances in Artificial Intelligence, 31st Annual German Conference on AI, KI 2008, Kaiserslautern, Germany, September 23-26, 2008. Proceedings, volume 5243 of Lecture Notes in Computer Science, pages 135-143. Springer, 2008.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Sofronie-Stokkermans, 2008c]
Viorica Sofronie-Stokkermans. Interpolation in local theory extensions. Logical Methods in Computer Science, 4(4):Article 1, 2008.
Abstract (click to open/close)

Subproject(s): R1,H3

Bibtex

PDF
restricted

[Sofronie-Stokkermans, 2008d]
Viorica Sofronie-Stokkermans. Locality and subsumption testing in EL and some of its extensions. In Advances in modal logic, Vol 7, pages 315-340. College Publications, 2008.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Sofronie-Stokkermans, 2008e]
Viorica Sofronie-Stokkermans. Locality and subsumption testing in EL and some of its extensions. In Franz Baader, Carsten Lutz, and Boris Motik, editors, Proceedings of the 21st International Workshop on Description Logics (DL2008), Dresden, Germany, May 13-16, 2008, volume 353 of CEUR Workshop Proceedings. CEUR-WS.org, 2008.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Sofronie-Stokkermans, 2008f]
Viorica Sofronie-Stokkermans. Sheaves and geometric logic and applications to modular verification of complex systems. AVACS Technical Report No.  46, SFB/TR 14 AVACS, December 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Swaminathan et al., 2008]
Mani Swaminathan, Martin Fränzle, and Joost-Pieter Katoen. The surprising robustness of (closed) timed automata against clock-drift. In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and Luke Ong, editors, The 5th IFIP International Conference on Theoretical Computer Science (IFIP TCS 2008). Sringer Verlag, September 2008.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Teige and Fränzle, 2008]
T. Teige and M. Fränzle. Stochastic satisfiability modulo theories for non-linear arithmetic. In L. Perron and M. A. Trick, editors, Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 5th International Conference, CPAIOR 2008, volume 5015 of Lecture Notes in Computer Science, pages 248-262. Springer, 2008.
Abstract (click to open/close)

Subproject(s): H1/2,H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Teige et al., 2008]
Tino Teige, Christian Herde, Martin Fränzle, and Erika Ábrahám. Conflict analysis and restarts in a mixed boolean and non-linear arithmetic constraint solver. AVACS Technical Report No.  34, SFB/TR 14 AVACS, January 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H1/2

Bibtex

PDF
open

[Toben, 2008]
Tobe Toben. Counterexample guided spotlight abstraction refinement. In Kenji Suzuki, Teruo Higashino, Keiichi Yasumoto, and Khaled El-Fakih, editors, Proceedings of the 28th IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2008), volume 5048 of LNCS, pages 21-36, Tokyo, Japan, June 2008. Springer-Verlag. Best Paper Award.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wehrle et al., 2008a]
Martin Wehrle, Sebastian Kupferschmid, and Andreas Podelski. Useless actions are useful. In Proceedings of the 18th International Conference on Automated Planning and Scheduling (ICAPS 2008), pages 388-395. AAAI Press, 2008.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open

[Wehrle et al., 2008b]
Martin Wehrle, Sebastian Kupferschmid, and Andreas Podelski. Useless transitions are useful. AVACS Technical Report No.  39, SFB/TR 14 AVACS, April 2008. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open

[Wilhelm and Wachter, 2008]
Reinhard Wilhelm and Björn Wachter. Abstract interpretation with applications to timing validation. In Aarti Gupta and Sharad Malik, editors, Proceedings of the 20th Int'l Conf. on Computer Aided Verification, CAV 2008, volume 5123 of Lecture Notes in Computer Science, pages 22-36. Springer Verlag, 2008. Princeton, NJ, USA.
Subproject(s): R2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wimmer et al., 2008a]
Ralf Wimmer, Salem Derisavi, and Holger Hermanns. Symbolic partition refinement with dynamic balancing of time and space. In Gerardo Rubino, editor, 5th International Conference on Quantitative Evaluation of Systems (QEST), pages 65-74, Saint-Malo, France, September 2008. IEEE Computer Science Press.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Wimmer et al., 2008b]
Ralf Wimmer, Alexander Kortus, Marc Herbstritt, and Bernd Becker. The demand for reliability in probabilistic verification. In Christoph Scholl and Stefan Disch, editors, Proceedings of the 11th GI/ITG/GMM-Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'' (MBMV), pages 99-108, Freiburg im Breisgau, Germany, March 2008. Shaker Verlag.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Wimmer et al., 2008c]
Ralf Wimmer, Alexander Kortus, Marc Herbstritt, and Bernd Becker. Probabilistic model checking and reliability of results. In Bernd Straube, Milos Drutarovsky, Michel Renovell, Peter Gramata, and Mária Fischerová, editors, 11th IEEE International Workshop on Design and Diagnostics of Electronic Circuits and Systems, pages 207-212, Bratislava, Slovakia, April 2008. IEEE Computer Science Press.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Witt, 2008]
Tobias Witt. Visualisierung von DPLL-basierten arithmetischen Constraint Solvern. Individuelles Projekt, Carl von Ossietzky Universität Oldenburg, Department für Informatik, 2008.
Abstract (click to open/close)

Subproject(s): H1,H2

Bibtex

PDF
open

[Zhang et al., 2008]
Lijun Zhang, Holger Hermanns, E. Moritz Hahn, and Björn Wachter. Time-bounded model checking of infinite-state continuous-time markov chains. In ACSD, 2008. Xi'an, China.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Ábrahám et al., 2007]
Erika Ábrahám, Marc Herbstritt, Bernd Becker, and Martin Steffen. Bounded model checking with parametric data structures. In Ofer Strichman and Armin Biere, editors, Proceedings of the Fourth International Workshop on Bounded Model Checking (BMC 2006), volume 174(3) of Electr. Notes Theor. Comput. Sci., pages 3-16, Seattle, WA, USA, August 2007. Elsevier.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PDF
restricted

[Badban et al., 2007]
Bahareh Badban, Jaco van de Pol, Olga Tveretina, and Hans Zantema. Generalizing DPLL and satisfiability for equalities. Journal of Information and Computation, 2007. to appear.
Abstract (click to open/close)

Keywords: satisfiability, DPLL procedure, equality, ground term algebra, inductive datatypes, decision procedure
Subproject(s): H1,H2

Bibtex

PDF
restricted

[Bauer, 2007]
Martin Bauer. Symbolic game solving with arithmetic data types, 2007. Bachelor Thesis.
Subproject(s): S1

Bibtex

PDF
open

[Bauer and Wilhelm, 2007]
Jörg Bauer and Reinhard Wilhelm. Static analysis of dynamic communication systems by partner abstraction. In Gilberto Filé and Hanne Riis Nielson, editors, Static Analysis Symposium, Springer LNCS, 2007.
Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Bauer et al., 2007a]
Jörg Bauer, Werner Damm, Tobe Toben, and Bernd Westphal. Verification and synthesis of ocl constraints via topology analysis. In Andy Schürr, Manfred Nagl, and Albert Zündorf, editors, Applications of Graph Transformations with Industrial Relevance, Third International Symposium, AGTIVE 2007, Revised Selected and Invited Papers, Kassel, Germany, volume 5088 of LNCS, pages 361-376. Springer-Verlag, October 2007.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Bauer et al., 2007b]
Jörg Bauer, Werner Damm, Tobe Toben, and Bernd Westphal. Verification and synthesis of OCL constraints via topology analysis: A case study. AVACS Technical Report No.  23, SFB/TR 14 AVACS, June 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Bauer et al., 2007c]
Jörg Bauer, Tobe Toben, and Bernd Westphal. Mind the shapes: Abstraction refinement via topology invariants. AVACS Technical Report No.  22, SFB/TR 14 AVACS, June 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Bauer et al., 2007d]
Jörg Bauer, Tobe Toben, and Bernd Westphal. Mind the shapes: Abstraction refinement via topology invariants. In 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007), LNCS, Tokyo, Japan, 2007. Springer-Verlag. to appear.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Bauer et al., 2007e]
Jörg Bauer, Tobe Toben, and Bernd Westphal. The temporal logic of appearance and disappearance. AVACS Technical Report No.  24, SFB/TR 14 AVACS, June 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Becker et al., 2007a]
Bernd Becker, Werner Damm, Martin Fränzle, Ernst-Rüdiger Olderog, Andreas Podelski, and Reinhard Wilhelm. SFB/TR 14 AVACS -- automatic verification and analysis of complex systems. it -- Information Technology, 49(2):118-126, 2007. http://it-Information-Technology.de, DOI 10.1524/itit.2007.49.2.118.
Abstract (click to open/close)

Subproject(s): R1,R2,R3,H1,H2,H3,H4,S1,S2,S3

Bibtex

PDF
open

[Becker et al., 2007b]
Bernd Becker, Christian Dax, Jochen Eisinger, and Felix Klaedtke. LIRA: Handling constraints of linear arithmetics over the integers and the reals. In Werner Damm and Holger Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification -- CAV 2007, volume 4590 of LNCS. Springer, 2007.
Abstract (click to open/close)

Subproject(s): H1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Behle and Eisenbrand, 2007]
Markus Behle and Friedrich Eisenbrand. 0/1 vertex and facet enumeration with bdds. In Workshop on Algorithm Engineering and Experiments (ALENEX 07), page to appear, New Orleans, USA, January 2007.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PDF
restricted

[Berdine et al., 2007]
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, Thomas Wies, and Hongseok Yang. Shape analysis for composite data structures. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, volume 4590 of Lecture Notes in Computer Science, pages 178-192. Springer-Verlag, July 2007.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Beyer et al., 2007a]
D. Beyer, T. Henzinger, R. Majumdar, and A.Rybalchenko. Invariant synthesis for combined theories. In VMCAI'2007: Verification, Model Checking, and Abstract Interpretation, volume 4349 of LNCS. Springer, 2007.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Beyer et al., 2007b]
Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Path invariants. In PLDI'2007: Programming Language Design and Implementation. ACM Press, 2007. to appear.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Bohnenkamp et al., 2007]
H. Bohnenkamp, H. Hermanns, and J. P. Katoen. Motor: The modest tool environment. In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, Lecture Notes in Computer Science, pages 500 -- 504, Braga, Portugal, 2007. Springer-Verlag.
Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Boudali et al., 2007]
H. Boudali, P. Crouzen, and M.I.A. Stoelinga. Dynamic fault tree analysis using input/output interactive markov chains. In International Conference on Dependable Systems and Networks, DSN07, 2007.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Bouillaguet et al., 2007]
Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin Rinard. Using first-order theorem provers in the Jahob data structure verification system. In Verification, Model Checking and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, volume 4349 of Lecture Notes in Computer Science, pages 74-88. Springer-Verlag, January 2007.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Brückner, 2007]
I. Brückner. Slicing concurrent real-time system specifications for verification. In J. Davies and J. Gibbons, editors, IFM 2007: Sixth International Conference on Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, pages 54-74. Springer-Verlag, July 2007.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Brückner et al., 2007]
Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Slicing abstractions. In Farhad Arbab and Marjan Sirjani, editors, Proceedings of the International Symposium on Fundamentals of Software Engineering (FSEN), 2007.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Burchardt and Ratschan, 2007]
Henning Burchardt and Stefan Ratschan. Estimating the region of attraction of ordinary differential equations by quantified constraint solving. In 3rd WSEAS International Conference on Dynamical Systems and Control (CONTROL'07), 2007. To appear.
Abstract (click to open/close)

Keywords: region of attraction, constraint solving
Subproject(s): H4

Bibtex

PDF
restricted

[Cook et al., 2007a]
Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Y. Vardi. Proving that programs eventually do something good. In POPL'2007: Principles of Programming Languages, pages 265-276. ACM Press, 2007.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted

[Cook et al., 2007b]
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving thread termination. In PLDI'2007: Programming Language Design and Implementation. ACM Press, 2007. to appear.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted

[Damm et al., 2007a]
W. Damm, S. Disch, H. Hungar, S. Jacobs, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Exact state set representation in the verification of linear hybrid systems with large discrete state space. AVACS Technical Report No.  21, SFB/TR 14 AVACS, June 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
open

[Damm et al., 2007b]
Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz. Exact state set representations in the verification of linear hybrid systems with large discrete state space. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, editors, Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, volume 4762 of Lecture Notes in Computer Science, pages 425-440, Tokyo, Japan, 2007. Springer.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Damm et al., 2007c]
Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken, and Boris Wirtz. Automating verification of cooperation, control, and design in traffic applications.. In Cliff Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pages 115-169. Springer, 2007.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Damm et al., 2007d]
Werner Damm, Guilherme Pinto, and Stefan Ratschan. Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. International Journal of Foundations of Computer Science, 18(1):63-88, February 2007.
Subproject(s): H3,H4

Bibtex

PDF
restricted

[Damm et al., 2007e]
Werner Damm, Tobe Toben, and Bernd Westphal. On the expressive power of Live Sequence Charts. In Thomas Reps, Mooly Sagiv, and Jörg Bauer, editors, Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm, number 4444 in Lecture Notes in Computer Science, pages 225-246. Springer-Verlag, 2007. To appear.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Dax et al., 2007]
Christian Dax, Jochen Eisinger, and Felix Klaedtke. Mechanizing the powerset construction for restricted classes of omega -automata. In Proc. of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07), Lecture Notes in Computer Science, pages 223-236, Berlin, Heidelberg, New York, 2007. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): H1,H2

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Dierks et al., 2007]
Henning Dierks, Sebastian Kupferschmid, and Kim G. Larsen. Automatic abstraction refinement for timed automata. In Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2007), Lecture Notes in Computer Science. Springer-Verlag, 2007. accepted for publication.
Abstract (click to open/close)


Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Disch and Scholl, 2007]
S. Disch and C. Scholl. Combinational equivalence checking using incremental SAT solving, output ordering, and resets. In ASP Design Automation Conf., jan 2007.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted

[Dragojevic, 2007]
Diana Dragojevic. Transformation von SPS- in Realzeitautomaten. Diplomarbeit, Albert-Ludwigs-Universität Freiburg, 2007.
Subproject(s): R3

Bibtex

PDF
open

[Faber and Stierand, 2007]
Johannes Faber and Ingo Stierand. From high-level verification to real-time scheduling: A property-preserving integration. AVACS Technical Report No.  19, SFB/TR 14 AVACS, June 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R1,R2

Bibtex

PDF
open

[Faber et al., 2007]
J. Faber, S. Jacobs, and V. Sofronie-Stokkermans. Verifying CSP-OZ-DC specifications with complex data types and timing parameters. In J. Davies and J. Gibbons, editors, Integrated Formal Methods 2007, volume 4591 of LNCS, pages 233-252, Berlin Heidelberg, 2007. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Ferdinand et al., 2007]
Christian Ferdinand, Florian Martin, Christoph Cullmann, Marc Schlickling, Ingmar Stein, Stephan Thesing, and Reinhold Heckmann. New developments in WCET analysis. In T. Reps, M. Sagiv, and J. Bauer, editors, Program Analysis and Compilation. Theory and Practice. Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, volume 4444 of LNCS, pages 12-52. Springer Verlag, 2007.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Finkbeiner and Schewe, 2007]
Bernd Finkbeiner and Sven Schewe. SMT-based synthesis of distributed systems. In Proc. AFM, 2007.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Fränzle and Hansen, 2007]
Martin Fränzle and Michael R. Hansen. Deciding an interval logic with accumulated durations. In Orna Grumberg and Michael Huth, editors, Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 07), volume 4424 of Lecture Notes in Computer Science, pages 201-215. Springer, 2007.
Abstract (click to open/close)

Keywords: Real-time systems, metric-time temporal logic, decidability, model-checking, multi-priced timed automata
Subproject(s): H1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Fränzle and Herde, 2007]
Martin Fränzle and Christian Herde. HySAT: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design, 30:179-198, 2007.
Abstract (click to open/close)

Keywords: verification, bounded model checking, hybrid systems, infinite-state systems, decision procedures, satisfiability
Subproject(s): H2

Bibtex

PostScript
restricted

PDF
restricted

[Fränzle et al., 2007a]
Martin Fränzle, Christian Herde, Stefan Ratschan, Tobias Schubert, and Tino Teige. Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation -- Special Issue on SAT/CP Integration, 1:209-236, 2007.
Abstract (click to open/close)

Subproject(s): H1,H2

Bibtex

PDF
restricted

[Fränzle et al., 2007b]
Martin Fränzle, Hardi Hungar, Christian Schmitt, and Boris Wirtz. Hlang: Compositional representation of hybrid systems via predicates. AVACS Technical Report No.  20, SFB/TR 14 AVACS, July 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H1/2,H3

Bibtex

PDF
open

[Gebhard and Altmeyer, 2007]
Gernot Gebhard and Sebastian Altmeyer. Optimal task placement to improve cache performance. In EMSOFT '07: Proceedings of the 7th ACM Conference on Embedded Systems Software, 2007. to appear.
Abstract (click to open/close)


Bibtex

PDF
restricted

[Groß et al., 2007]
Christian Groß, Holger Hermanns, and Reza Pulungan. Does clock precision influence ZigBee's energy consumptions?. AVACS Technical Report No.  17, SFB/TR 14 AVACS, May 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Keywords: sensor network, energy consumption, ZigBee, stochastic modelling
Subproject(s): S3

Bibtex

PDF
open

[Haddad, 2007]
Walid Haddad. Inequality constraints on synchronization counters. Bachelor thesis, Universität des Saarlandes, 2007.
Subproject(s): R3

Bibtex

PDF
open

[Helmert et al., 2007]
Malte Helmert, Patrik Haslum, and Jörg Hoffmann. Flexible abstraction heuristics for optimal sequential planning. In Proceedings of the 17th International Conference on Automated Planning and Scheduling (ICAPS 2007), pages 176-183. AAAI Press, 2007.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
restricted

[Herbstritt and Becker, 2007]
Marc Herbstritt and Bernd Becker. On combining 01X-logic and QBF. In Roberto Moreno-Díaz and Franz Pichler, editors, Proceedings of 11th International Conference on Computer Aided Systems Theory (EUROCAST), volume 4739 of Lecture Notes in Computer Science, pages 531-538, Las Palmas de Gran Canaria, Canary Islands, Spain, February 2007. Springer-Verlag. Applied Formal Verification Track, Revised Selected Papers.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Herbstritt et al., 2007a]
Marc Herbstritt, Bernd Becker, Erika Ábrahám, and Christian Herde. On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata. In Proceedings of the IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS), pages 391-396, Kraków, Poland, 2007. IEEE Computer Society.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PDF
restricted

[Herbstritt et al., 2007b]
Marc Herbstritt, Vanessa Struve, and Bernd Becker. Application of lifting in partial design analysis. In Proc. of Microprocessor Test and Verification Workshop (MTV), pages 33-38, Austin (TX), USA, Dec. 2007. IEEE Computer Society.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Hermanns and Johr, 2007]
Holger Hermanns and Sven Johr. Uniformity by construction in the analysis of nondeterministic stochastic systems. In International Conference on Dependable Systems and Networks, DSN07, 2007.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Hermanns et al., 2007]
Holger Hermanns, Björn Wachter, and Lijun Zhang. On probabilistic CEGAR. AVACS Technical Report No.  33, SFB/TR 14 AVACS, December 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Hobelmann, 2007]
U. Hobelmann. Verifying properties of processes, data, and time: Linking counterexamples to high-level specifications. Master's thesis, University of Oldenburg, 2007.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Jacobs and Sofronie-Stokkermans, 2007]
Swen Jacobs and Viorica Sofronie-Stokkermans. Applications of hierarchical reasoning in the verification of complex systems. Electronic Notes in Theoretical Computer Science, 174(8):39-54, 2007.
Subproject(s): R1

Bibtex

PDF
restricted

[Jacobs and Waldmann, 2007]
Swen Jacobs and Uwe Waldmann. Comparing instance generation methods for automated reasoning. Journal of Automated Reasoning, 38:57-78, April 2007.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted

[Jung, 2007]
Dennis Jung. Eine automatentheoretische Heuristik für klassische Planungsprobleme. Diplomarbeit, Albert-Ludwigs-Universität Freiburg, 2007.
Subproject(s): R3

Bibtex

PDF
open

[Klaedtke, 2007]
Felix Klaedtke. Bounds on the automata size for Presburger arithmetic. ACM Transactions on Computational Logic, 2007. Accepted for publication.
Abstract (click to open/close)

Subproject(s): H1

Bibtex

PDF
restricted

[Klaedtke et al., 2007]
Felix Klaedtke, Stefan Ratschan, and Zhikun She. Language-based abstraction refinement for hybrid system verification. In 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), volume 4349 of Lecture Notes in Computer Science. Springer-Verlag, 2007. Accepted for publication.
Abstract (click to open/close)

Subproject(s): H1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Kupferschmid et al., 2007]
Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, and Gerd Behrmann. Uppaal/DMC -- abstraction-based heuristics for directed model checking. In Orna Grumberg and Michael Huth, editors, Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4424 of Lecture Notes in Computer Science, pages 679-682, Berlin Heidelberg, 2007. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Nopper and Scholl, 2007a]
T. Nopper and C. Scholl. Counterexample generation for incomplete designs. In GI/ITG/GMM Workshop``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', 2007.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Nopper and Scholl, 2007b]
Tobias Nopper and Christoph Scholl. Symbolic model checking for incomplete designs with flexible modeling of unknowns. AVACS Technical Report No.  31, SFB/TR 14 AVACS, July 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Nopper et al., 2007]
Tobias Nopper, Christoph Scholl, and Bernd Becker. Computation of minimal counterexamples by using black box techniques and symbolic methods. In International Conference on Computer Aided Design (ICCAD), 2007. To appear.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Oehlerking et al., 2007]
Jens Oehlerking, Henning Burchardt, and Oliver Theel. Fully automated stability verification for piecewise affine systems. In Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo, editors, 10th IEEE International Conference on Hybrid Systems: Computations and Control, volume 4416 of Lecture Notes in Computer Science. Springer, 2007.
Abstract (click to open/close)

Keywords: piecewise affine systems, stability verification, linear matrix inequalities
Subproject(s): H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Platzer, 2007a]
André Platzer. Combining deduction and algebraic constraints for hybrid system analysis.. In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, CEUR Workshop Proceedings. CEUR-WS.org, 2007.
Abstract (click to open/close)

Keywords: modular prover combination, analytic tableaux, verification of hybrid systems, dynamic logic
Subproject(s): H3

Bibtex

PDF
open

[Platzer, 2007b]
André Platzer. Differential dynamic logic for verifying parametric hybrid systems. AVACS Technical Report No.  15, SFB/TR 14 AVACS, May 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Keywords: Dynamic logic, sequent calculus, verification of parametric hybrid systems, quantifier elimination
Subproject(s): H3

Bibtex

PDF
open

[Platzer, 2007c]
AndréPlatzer. Differential dynamic logic for verifying parametric hybrid systems.. In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pages 216-232. Springer, 2007. This paper was awarded the Tableaux Best Paper Award.
Abstract (click to open/close)

Keywords: dynamic logic, sequent calculus, verification of parametric hybrid systems, quantifier elimination
Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Platzer, 2007d]
André Platzer. Differential logic for reasoning about hybrid systems.. In Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of Lecture Notes in Computer Science, pages 746-749. Springer, 2007.
Abstract (click to open/close)

Keywords: dynamic logic, hybrid systems, parametric verification
Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Platzer, 2007e]
André Platzer. A temporal dynamic logic for verifying hybrid system invariants.. AVACS Technical Report No.  12, SFB/TR 14 AVACS, February 2007. ISSN: 1860-9821, http://www.avacs.org, long version of  [Platzer, 2007f].
Abstract (click to open/close)

Keywords: dynamic logic, sequent calculus, logic for hybrid systems, temporal logic, deductive verification of embedded systems
Subproject(s): H3

Bibtex

PDF
open

[Platzer, 2007f]
André Platzer. A temporal dynamic logic for verifying hybrid system variants. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pages 457-471. Springer, 2007.
Abstract (click to open/close)

Keywords: dynamic logic, sequent calculus, logic for hybrid systems, temporal logic, deductive verification of embedded systems
Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Platzer and Clarke, 2007]
A. Platzer and E. M. Clarke. The image computation problem in hybrid systems model checking.. In Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of Lecture Notes in Computer Science, pages 473-486. Springer, 2007.
Abstract (click to open/close)

Keywords: model checking, hybrid systems, image computation
Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Podelski and Rybalchenko, 2007]
Andreas Podelski and Andrey Rybalchenko. ARMC: the logical choice for software model checking with abstraction refinement. In M. Hanus, editor, PADL'2007: Practical Aspects of Declarative Languages, volume 4354 of LNCS, pages 245-259. Springer, 2007.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Podelski and Wagner, 2007a]
Andreas Podelski and Silke Wagner. Region stability proofs for hybrid systems. In Formal Modelling and Analysis of Timed Systems, FORMATS'07, 2007. to appear.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted

[Podelski and Wagner, 2007b]
Andreas Podelski and Silke Wagner. A sound and complete proof rule for region stability of hybrid systems. In Proceedings of the 10th Conference on Hybrid Systems: Computation and Control, volume 4416 of Lecture Notes in Computer Science, pages 750 -- 753, 2007.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Pulungan and Hermanns, 2007]
Reza Pulungan and Holger Hermanns. A method for reducing acyclic phase-type representations. AVACS Technical Report No.  32, SFB/TR 14 AVACS, July 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Quesel, 2007]
Jan-David Quesel. A theorem prover for differential dynamic logic: Deductive verification of hybrid systems. Master's thesis, University of Oldenburg, Department of Computing Science. Correct System Design Group, Apr 2007.
Subproject(s): H3

Bibtex

[Ratschan and She, 2007]
Stefan Ratschan and Zhikun She. Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Transactions on Embedded Computing Systems, 6(1), 2007.
Abstract (click to open/close)

Subproject(s): H1

Bibtex

PDF
restricted

[Reineke et al., 2007]
Jan Reineke, Daniel Grund, Christoph Berg, and Reinhard Wilhelm. Timing predictability of cache replacement policies. Real-Time Systems, 2007.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Rybalchenko and Sofronie-Stokkermans, 2007]
Andrey Rybalchenko and Viorica Sofronie-Stokkermans. Constraint solving for interpolation. In Byron Cook and Andreas Podelski, editors, 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), volume 4349 of Lecture Notes in Computer Science. Springer, 2007.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Schewe, 2007a]
Sven Schewe. An optimal strategy improvement algorithm for solving parity games. AVACS Technical Report No.  28, SFB/TR 14 AVACS, July 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Schewe, 2007b]
Sven Schewe. Solving parity games in big steps. AVACS Technical Report No.  26, SFB/TR 14 AVACS, July 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Schewe, 2007c]
Sven Schewe. Solving parity games in big steps. In Foundations of Software Technology and Theoretical Computer Science, 27th International Conference (FSTTCS 2007). Springer Verlag, 2007.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Schewe and Finkbeiner, 2007a]
Sven Schewe and Bernd Finkbeiner. Bounded synthesis. AVACS Technical Report No.  27, SFB/TR 14 AVACS, July 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Schewe and Finkbeiner, 2007b]
Sven Schewe and Bernd Finkbeiner. Bounded synthesis. In 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007). Springer Verlag, 2007. accepted for publication.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Schewe and Finkbeiner, 2007c]
Sven Schewe and Bernd Finkbeiner. Distributed synthesis for alternating-time logics. AVACS Technical Report No.  25, SFB/TR 14 AVACS, July 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Schewe and Finkbeiner, 2007d]
Sven Schewe and Bernd Finkbeiner. Distributed synthesis for alternating-time logics. In 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007). Springer Verlag, 2007. accepted for publication.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Schewe and Finkbeiner, 2007e]
Sven Schewe and Bernd Finkbeiner. Semi-automatic distributed synthesis. International Journal of Foundations of Computer Science (IJFCS), 18(1):113-138, February 2007.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PostScript
restricted

PDF
restricted

[Schlickling and Pister, 2007]
Marc Schlickling and Markus Pister. A framework for static analysis of VHDL code. In Proceedings of 7th International Workshop on Worst-Case Execution Time (WCET) Analysis, July 2007.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Segelken, 2007]
Marc Segelken. Abstraction and counterexample-guided construction of omega-automata for model checking of step-discrete linear hybrid models. In Werner Damm and Holger Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification -- CAV 2007, volume 4590 of LNCS. Springer, 2007.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Smaus, 2007a]
Jan-Georg Smaus. On Boolean functions encodable as a single linear pseudo-Boolean constraint. AVACS Technical Report No.  13, SFB/TR 14 AVACS, March 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PDF
open

[Smaus, 2007b]
Jan-Georg Smaus. On boolean functions encodable as a single linear pseudo-boolean constraint. In Pascal Van Hentenryck and Laurence Wolsey, editors, Proceedings of the 4th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, volume 4510 of LNCS, pages 288-302. Springer-Verlag, 2007. Long version available as ATR No. 13 on url http://www.avacs.org/.
Subproject(s): R3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Sofronie-Stokkermans, 2007a]
Viorica Sofronie-Stokkermans. Automated theorem proving by resolution in non-classical logics. Annals of Mathematics and Artificial Intelligence (Special issue Knowledge Discovery and Discrete Mathematics: Dedicated to the Memory of Peter L. Hammer), 49(1-4):221-252, 2007.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Sofronie-Stokkermans, 2007b]
Viorica Sofronie-Stokkermans. Hierarchical and modular reasoning in complex theories: The case of local theory extensions. In 6th International Symposium on Frontiers of Combining Systems (FROCOS), volume 4720 of LNCS, pages 47-71, Liverpool, England, 2007. Springer.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Sofronie-Stokkermans, 2007c]
Viorica Sofronie-Stokkermans. On unification for bounded distributive lattices. ACM Transactions on Computational Logic, 8(2), 2007.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Sofronie-Stokkermans and Ihlemann, 2007a]
Viorica Sofronie-Stokkermans and Carsten Ihlemann. Automated reasoning in some local extensions of ordered structures. In Proceedings of ISMVL 2007, Oslo, Norway, 2007. IEEE. To appear.
Abstract (click to open/close)

Subproject(s): R1,H3

Bibtex

PDF
restricted

[Sofronie-Stokkermans and Ihlemann, 2007b]
Viorica Sofronie-Stokkermans and Carsten Ihlemann. Automated reasoning in some local extensions of ordered structures. Journal of Multiple-Valued Logic, 2007. To appear; 18 pages.
Abstract (click to open/close)

Subproject(s): R1,H3

Bibtex

PDF
restricted

[Sofronie-Stokkermans et al., 2007]
Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs. Local theory extensions, hierarchical reasoning and applications to verification. In Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis, editors, Deduction and Decision Procedures, number 07401 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2007. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany.
Abstract (click to open/close)

Keywords: Automated reasoning, Combinations of decision procedures, Verification
Subproject(s): R1

Bibtex

PDF
restricted

[Stierand and Metzner, 2007]
Ingo Stierand and Alexander Metzner. A mode change protocol for distributed real-time systems. AVACS Technical Report No.  11, SFB/TR 14 AVACS, February 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Stierand et al., 2007]
Ingo Stierand, Henning Dierks, and Alexander Metzner. Combining timed automata based formal specifications and real-time scheduling analysis. AVACS Technical Report No.  18, SFB/TR 14 AVACS, June 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Swaminathan and Fränzle, 2007]
Mani Swaminathan and Martin Fränzle. A symbolic decision procedure for robust safety of timed systems. In proceedings on the 14th International Symposium on Temporal Representation and Reasoning (TIME 2007). IEEE CS Press, 2007. To appear as a short paper/poster.
Abstract (click to open/close)

Subproject(s): H1

Bibtex

PDF
restricted

[Teige et al., 2007]
Tino Teige, Christian Herde, Martin Fränzle, Natalia Kalinnik, and Andreas Eggers. A generalized two-watched-literal scheme in a mixed boolean and non-linear arithmetic constraint solver. In José Neves, Manuel Filipe Santos, and José Manuel Machado, editors, Proceedings of the 13th Portuguese Conference on Artificial Intelligence (EPIA 2007), New Trends in Artificial Intelligence, pages 729-741. APPIA, December 2007.
Abstract (click to open/close)

Subproject(s): H1, H2

Bibtex

PDF
restricted

[Toben, 2007]
Tobe Toben. Non-interference properties for data-type reduction of communicating systems. In J. Davies and J. Gibbons, editors, Proceedings of the Sixth International Conference on Integrated Formal Methods (IFM 2007), volume 4591 of LNCS, pages 619-638, Oxford, UK, July 2007. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wachter and Westphal, 2007]
Björn Wachter and Bernd Westphal. The spotlight principle. on combining process-summarizing state abstractions. In Byron Cook and Andreas Podelski, editors, Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings, volume 4349 of Lecture Notes in Computer Science, pages 182-198. Springer-Verlag, 2007.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wachter et al., 2007]
Björn Wachter, Lijun Zhang, and Holger Hermanns. Probabilistic model checking modulo theories. In Fourth International Conference on the Quantitative Evaluation of Systems. IEEE CS press, 2007.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Wilhelm and Wachter, 2007]
Stephan Wilhelm and Björn Wachter. Towards symbolic state traversal for Efficient WCET analysis of abstract pipeline and cache models. In Proceedings of 7th International Workshop on Worst-Case Execution Time (WCET) Analysis, July 2007.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Wilhelm et al., 2007a]
Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter Puschner, Jan Staschulat, and Per Stenström. The worst-case execution time problem -- overview of methods and survey of tools. AVACS Technical Report No.  14, SFB/TR 14 AVACS, April 2007. ISSN: 1860-9821, http://www.avacs.org; This is the author's version of an article to appear in ACM Transactions in Embedded Computing Systems.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Wilhelm et al., 2007b]
Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Frank Mueller, Isabelle Puaut, Peter Puschner, Jan Staschulat, , and Per Stenströ¶. The determination of worst-case execution times --- overview of the methods and survey of tools. accepted for ACM Transactions on Embedded Computing Systems (TECS), 2007.
Subproject(s): R2

Bibtex

PDF
restricted

[Wimmer et al., 2007a]
Ralf Wimmer, Marc Herbstritt, and Bernd Becker. Forwarding, splitting, and block ordering to optimize BDD-based bisimulation computation. In Christian Haubelt and Jürgen Teich, editors, Proceedings of the 10 textsuperscript th GI/ITG/GMM-Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'' (MBMV), pages 203-212, Erlangen, Germany, March 2007. Shaker Verlag.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Wimmer et al., 2007b]
Ralf Wimmer, Marc Herbstritt, and Bernd Becker. Optimization techniques for bdd-based bisimulation minimization. In Hai Zhou and Enrico Macii, editors, Proceedings of the 17th ACM Great Lakes Symposium on VLSI, Stresa, Italy, 2007. ACM Press.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Wimmer et al., 2007c]
Ralf Wimmer, Holger Hermanns, Marc Herbstritt, and Bernd Becker. Towards symbolic stochastic aggregation. AVACS Technical Report No.  16, SFB/TR 14 AVACS, August 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Wimmer et al., 2007d]
Ralf Wimmer, Alexander Kortus, Marc Herbstritt, and Bernd Becker. Symbolic Model Checking for DTMCs with Exact and Inexact Arithmetic. AVACS Technical Report No.  30, SFB/TR 14 AVACS, August 2007. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Wischnewski, 2007]
Patrick Wischnewski. SBDD - representing sets of boolean functions, 2007. Bachelor Thesis.
Subproject(s): S1

Bibtex

PDF
open

[Zhang et al., 2007]
L. Zhang, H. Hermanns, F. Eisenbrand, and D. N. Jansen. Flow faster: Efficient decision algorithms for probabilistic simulations. In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, Lecture Notes in Computer Science, pages 155-169, Braga, Portugal, 2007. Springer-Verlag. Invited to LMCS special issue of TACAS 2007.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Ábrahám et al., 2006a]
Erika Ábrahám, Marc Herbstritt, Bernd Becker, and Martin Steffen. Memory-aware bounded model checking for linear hybrid systems. In Bernd Straube, editor, ITG/GI/GMM-Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', pages 153-162, Feb 2006. ISBN 3-9810287-1-6.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PDF
restricted

[Ábrahám et al., 2006b]
Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, and Christian Herde. Parallel SAT solving in bounded model checking. In Proc. of PDMC'06, Lecture Notes in Computer Science. Springer Verlag, 2006.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Badban et al., 2006]
Bahareh Badban, Martin Fränzle, Jan Peleska, and Tino Teige. Test automation for hybrid systems. In Proceedings of the Third International Workshop on SOFTWARE QUALITY ASSURANCE (SOQUA 2006), pages 14-21, Portland Oregon, USA, November 2006.
Abstract (click to open/close)

Subproject(s): H1,H2

Bibtex

PDF
restricted

[Bauer, 2006]
Jörg Bauer. Analysis of Communication Topologies by Partner Abstraction. PhD thesis, Universität des Saarlandes, 2006.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Bauer et al., 2006]
Joerg Bauer, Ina Schaefer, Tobe Toben, and Bernd Westphal. Specification and verification of dynamic communication systems. In Kees Goossens and Laure Petrucci, editors, Proceedings of the 6th International Conference on Application of Concurrency to System Design (ACSD 2006), Turku, Finland, June 2006. IEEE.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Berg, 2006]
Christoph Berg. PLRU cache domino effects. In Frank Mueller, editor, 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Dresden, number 06902 in Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), July 2006.
Abstract (click to open/close)

Keywords: Keywords: Embedded systems, predictability, cache memory, PLRU, domino effects, timing anomalies
Subproject(s): R2

Bibtex

PDF
restricted

[Böde et al., 2006]
Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, and Bernd Becker. Compositional performability evaluation for statemate. In 3rd International Conference on the Quantitative Evaluation of Systems, QEST 2006, Riverside (USA), pages 167-178. IEEE Computer Society, 2006.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Brückner et al., 2006]
I. Brückner, B. Metzler, and H. Wehrheim. Optimizing slicing of formal specifications by deductive verification. Nordic Journal of Computing, 13(1-2):22-45, August 2006.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Burchardt et al., 2006]
Henning Burchardt, Jens Oehlerking, and Oliver Theel. Developing a tool for automatic stability verification of hybrid systems. Poster Session, 1st Workshop on Feedback Control Implementation and Design in Computing Systems and Networks (FeBID '06), 2006.
Subproject(s): H4

Bibtex

PostScript
restricted

[Cook et al., 2006a]
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination proofs for systems code. In PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, pages 415-426, New York, NY, USA, 2006. ACM Press.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
open

[Cook et al., 2006b]
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Terminator: Beyond safety. In Thomas Ball and Robert B. Jones, editors, CAV'06" --- Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 415-418. Springer, 2006.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Damm et al., 2006a]
W. Damm, S. Disch, H. Hungar, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Automatic verification of hybrid systems with large discrete state space. In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis, volume 4218 of Lecture Notes in Computer Science. Springer-Verlag, 2006.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Damm et al., 2006b]
W. Damm, H. Hungar, and E.-R. Olderog. Verification of cooperating traffic agents. International Journal of Control, 79(5):395 -- 421, May 2006.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted

[Dhama et al., 2006a]
Abhishek Dhama, Jens Oehlerking, and Oliver Theel. Verification of orbitally self-stabilizing distributed algorithms using lyapunov functions and poincare maps. In Joseph L. Hellerstein, Xiaoyun Zhu, and Tarek Abdelzaher, editors, 1st Workshop on Feedback Control Implementation and Design in Computing Systems and Networks (FeBID '06). IEEE Communications Society, April 2006.
Keywords: Fault Tolerance, Self-Stabilization, Verification, Hybrid Systems, Lyapunov Theory, Poincare Maps
Subproject(s): H4

Bibtex

PDF
restricted

[Dhama et al., 2006b]
Abhishek Dhama, Jens Oehlerking, and Oliver Theel. Verification of orbitally self-stabilizing distributed algorithms using Lyapunov functions and Poincaré maps. In Twelfth International Conference on Parallel and Distributed Systems, pages 23 -- 30. IEEE Computer Society, 2006. Improved version of the paper published at FeBID'06.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted

[Dräger et al., 2006]
Klaus Dräger, Bernd Finkbeiner, and Andreas Podelski. Directed model checking with distance-preserving abstractions.. In Antti Valmari, editor, Model Checking Software, 13th International SPIN Workshop, volume 3925 of LNCS, pages 19-34. Springer, 2006.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Eggers, 2006]
Andreas Eggers. Einbettung sicherer numerischer Integration von Differentialgleichungen in DPLL-basiertes arithmetisches Constraint-Solving für hybride Systeme. Master's thesis, Carl von Ossietzky Universität Oldenburg, Department für Informatik, 2006.
Abstract (click to open/close)

Subproject(s): H1,H2

Bibtex

PDF
open

[Eisenbrand et al., 2006]
F. Eisenbrand, W. Damm, A. Metzner, G. Shmonin, R. Wilhelm, and S. Winkel. Mapping Task-Graphs on Distributed ECU Networks: Efficient Algorithms for Feasibility and Optimality. In Proceedings of the 12th IEEE Conference on Embedded and Real-Time Computing Systems and Applications. IEEE Computer Society, 2006.
Subproject(s): R2

Bibtex

PDF
restricted

[Eisinger and Klaedtke, 2006]
Jochen Eisinger and Felix Klaedtke. Don't care words with application to the automata-based approach for real addition. In Proc. of the 18th International Conference on Computer Aided Verification (CAV'06), Lecture Notes in Computer Science, 2006.
Abstract (click to open/close)

Subproject(s): H1

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Eisinger et al., 2006]
J. Eisinger, I. Polian, B. Becker, A. Metzner, S. Thesing, and R. Wilhelm. Automatic Identification of Timing Anomalies for Cycle-Accurate Worst-Case Execution Time Analysis. In Proceedings of the 9th IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems. IEEE Computer Society, 2006.
Abstract (click to open/close)

Keywords: Real-time system verification, Worst-case execution time (WCET), Timing anomalies, Formal methods
Subproject(s): R2

Bibtex

PDF
restricted

[Faber and Meyer, 2006]
J. Faber and R. Meyer. Model checking data-dependent real-time properties of the european train control system. In Formal Methods in Computer Aided Design, pages 76-77. IEEE Computer Society, nov 2006.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted

[Fietzke, 2006]
Arnaud Fietzke. Learning minimal requirements for compositional verification. Bachelor thesis, Universität des Saarlandes, Germany, November 2006.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Finkbeiner et al., 2006]
Bernd Finkbeiner, Sven Schewe, and Matthias Brill. Automatic synthesis of assumptions for compositional model checking. In 26th International Conference on Formal Methods for Networked and Distributed Systems (FORTE 2006), pages 143-158. Springer Verlag, 2006.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Fränzle et al., 2006]
Martin Fränzle, Christian Herde, Stefan Ratschan, Tobias Schubert, and Tino Teige. Interval constraint solving using propositional SAT solving techniques. In Proceedings of the CP 2006 First International Workshop on the Integration of SAT and CP Techniques, pages 81-95, 2006.
Abstract (click to open/close)

Subproject(s): H1,H2

Bibtex

PDF
open

[Ganzinger et al., 2006]
Harald Ganzinger, Viorica Sofronie-Stokkermans, and Uwe Waldmann. Modular proof systems for partial functions with Evans equality. Information and Computation, 204(10):1453-1492, 2006.
Subproject(s): R1,H3

Bibtex

PDF
restricted

[Helmert, 2006a]
Malte Helmert. The Fast Downward planning system. Journal of Artificial Intelligence Research, 26:191-246, 2006.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Helmert, 2006b]
Malte Helmert. Solving Planning Tasks in Theory and Practice. PhD thesis, Albert-Ludwigs-Universität Freiburg, 2006.
Subproject(s): S1

Bibtex

PDF
open

[Helmert et al., 2006]
Malte Helmert, Robert Mattmüller, and Sven Schewe. Selective approaches for solving weak games. In Proceedings of the Fourth International Symposium on Automated Technology for Verification and Analysis (ATVA 2006), pages 200-214, 2006.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Herbstritt et al., 2006a]
Marc Herbstritt, Bernd Becker, and Christoph Scholl. Advanced SAT-techniques for bounded model checking of blackbox designs. In Proc. of Microprocessor Test and Verification Workshop (MTV), pages 37-44, Austin (TX), USA, Dec. 2006. IEEE Computer Society.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Herbstritt et al., 2006b]
Marc Herbstritt, Ralf Wimmer, Thomas Peikenkamp, Eckard Böde, Michael Adelaide, Sven Johr, Holger Hermanns, and Bernd Becker. Analysis of Large Safety-Critical Systems: A quantitative Approach. AVACS Technical Report No.  8, SFB/TR 14 AVACS, Feb 2006. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Hoffmann et al., 2006]
Jörg Hoffmann, Jan-Georg Smaus, Andrey Rybalchenko, Sebastian Kupferschmid, and Andreas Podelski. Using predicate abstraction to generate heuristic functions in uppaal. In Stefan Edelkamp and Alessio R. Lomuscio, editors, Post-Proceedings of the 4th Workshop on Model Checking and Artificial Intelligence (MoChArt 2006), 2006.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
restricted

[Jacobs and Sofronie-Stokkermans, 2006]
Swen Jacobs and Viorica Sofronie-Stokkermans. Applications of hierarchical reasoning in the verification of complex systems. In Proceedings of the Fourth International Workshop on Pragmatics of Decision Procedures in Automated Reasoning, pages 15-26, 2006.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Karro, 2006]
Baltin Karro. Entwicklung eines werkzeugs zur klassifizierung von hybriden systemen. Master's thesis, University of Oldenburg, 2006.
Subproject(s): H4

Bibtex

PDF
open

[Kemper, 2006]
Stephanie Kemper. SAT-based verification for abstraction-refinement. Master's thesis, University of Oldenburg, Department of Computing Science. Correct System Design Group, Jan 2006.
Subproject(s): H3

Bibtex

[Kemper and Platzer, 2006]
Stephanie Kemper and André Platzer. SAT-based abstraction refinement for real-time systems. In Frank S. de Boer and Vladimir Mencl, editors, Proc., International Workshop on Formal Aspects of Component Software (FACS'06), Prague, Czech Republic, ENTCS, 2006.
Abstract (click to open/close)

Keywords: abstraction refinement, model checking, real-time systems, SAT, Craig interpolation
Subproject(s): R3

Bibtex

PDF
open

[Klose et al., 2006]
Jochen Klose, Tobe Toben, Bernd Westphal, and Hartmut Wittke. Check it out: On the efficient formal verification of Live Sequence Charts. In T. Ball and R. B. Jones, editors, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, USA, August 16-21, 2006, Proceedings, number 4144 in LNCS, pages 219-233. Springer-Verlag, August 2006.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Kupferschmid et al., 2006]
Sebastian Kupferschmid, Jörg Hoffmann, Henning Dierks, and Gerd Behrmann. Adapting an AI planning heuristic for directed model checking. In Antti Valmari, editor, Model Checking Software. Proceedings of the 13th International SPIN Workshop (SPIN2006), volume 3925 of Lecture Notes in Computer Science, pages 35-52. Springer-Verlag, April 2006.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Lisagor et al., 2006]
O. Lisagor, M. Pretzer, C. Seguin, D. J. Pumfrey, F. Iwu, and T. Peikenkamp. Towards Safety Analysis of Highly Integrated Technologically Heterogeneous Systems -- A Domain-Based Approach for Modelling System Failure Logic. In Proceedings of the 24th International System Safety Conference (ISSC), Albuquerque, New Mexico, USA, 2006.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Metzner and Herde, 2006]
Alexander Metzner and Christian Herde. Rtsat --- an optimal and efficient approach to the task allocation problem in distributed architectures. In Proceedings of the IEEE Real-Time Systems Symposium, pages 147 -- 156. IEEE Computer Society, 2006.
Abstract (click to open/close)

Subproject(s): R2,H2

Bibtex

PDF
restricted

[Metzner et al., 2006]
A. Metzner, M. Fränzle, C. Herde, and I. Stierand. An Optimal Approach to the Task Allocation Problem on Hierarchical Architectures. In Proceedings of the 20th IEEE International Parallel and Distributed Processing Symposium. IEEE Computer Society, 2006.
Abstract (click to open/close)

Subproject(s): R2,H2

Bibtex

PDF
restricted

[Meyer et al., 2006]
R. Meyer, J. Faber, and A. Rybalchenko. Model checking duration calculus: A practical approach. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, Theoretical Aspects of Computing - ICTAC 2006, volume 4281 of LNCS, pages 332-346, Berlin / Heidelberg, 2006. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Pigorsch et al., 2006a]
F. Pigorsch, C. Scholl, and S. Disch. Advanced unbounded CTL model checking by using AIGs, BDD sweeping, and quantifier scheduling. In GI/ITG/GMM Workshop``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', pages 135-144, Feb 2006.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted

[Pigorsch et al., 2006b]
F. Pigorsch, C. Scholl, and S. Disch. Advanced unbounded model checking based on AIGs, BDD sweeping, and quantifier scheduling. In Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD), pages 89-96. IEEE Computer Society Press, Nov 2006.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted

[Platzer, 2006]
André Platzer. Towards a hybrid dynamic logic for hybrid dynamic systems. In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva, and Jørgen Villadsen, editors, Proc., LICS International Workshop on Hybrid Logic, Seattle, USA, ENTCS, 2006.
Abstract (click to open/close)

Keywords: hybrid logic, dynamic logic, sequent calculus, compositional verification, real-time hybrid dynamic systems
Subproject(s): H3

Bibtex

PDF
open

[Podelski and Wagner, 2006]
Andreas Podelski and Silke Wagner. Model checking of hybrid systems: From reachability towards stability. In Hybrid Systems: Computation and Control, HSCC'06, volume 3927 of Lecture Notes in Computer Science, pages 507 -- 521, 2006.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
open
© Springer Verlag (see article at SpringerLink)

[Pulungan and Hermanns, 2006]
Reza Pulungan and Holger Hermanns. Orthogonal distance fitting for phase-type distributions. AVACS Technical Report No.  10, SFB/TR 14 AVACS, November 2006. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Ratschan, 2006]
Stefan Ratschan. Verification of hybrid systems. Newsletter of the European Consortium for Mathematics in Industry (ECMI), 39:13-14, 2006.
Subproject(s): H1

Bibtex

PDF
restricted

[Ratschan and She, 2006a]
Stefan Ratschan and Zhikun She. Constraints for continuous reachability in the verification of hybrid systems. In Proc. of the 8th International Conference on Artificial Intelligence and Symbolic Computation, AISC'2006, LNCS. Springer, 2006.
Abstract (click to open/close)

Subproject(s): H1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Ratschan and She, 2006b]
Stefan Ratschan and Zhikun She. Providing a basin of attraction to a target region by computation of Lyapunov-like functions. In IEEE International Conference on Computational Cybernetics, 2006. accepted.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted

[Ratschan and Smaus, 2006]
Stefan Ratschan and Jan-Georg Smaus. Verification-integrated falsification of non-deterministic hybrid systems. In Proceedings of the 2nd IFAC Conference on Analysis and Design of Hybrid Systems, 2006.
Abstract (click to open/close)

Subproject(s): H1

Bibtex

PDF
restricted

[Reineke et al., 2006a]
Jan Reineke, Daniel Grund, Christoph Berg, and Reinhard Wilhelm. Predictability of cache replacement policies. AVACS Technical Report No.  9, SFB/TR 14 AVACS, September 2006. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Reineke et al., 2006b]
Jan Reineke, Björn Wachter, Stephan Thesing, Reinhard Wilhelm, Ilia Polian, Jochen Eisinger, and Bernd Becker. A definition and classification of timing anomalies. In Proceedings of 6th International Workshop on Worst-Case Execution Time (WCET) Analysis, July 2006.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Schewe, 2006]
Sven Schewe. Synthesis for probabilistic environments. In 4th International Symposium on Automated Technology for Verification and Analysis (ATVA 2006), pages 245-259. Springer Verlag, 2006.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Schewe and Finkbeiner, 2006a]
Sven Schewe and Bernd Finkbeiner. Satisfiability and finite model property for the alternating-time mu -calculus. In 15th Annual Conference on Computer Science Logic (CSL 2006), pages 591-605. Springer Verlag, 2006.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Schewe and Finkbeiner, 2006b]
Sven Schewe and Bernd Finkbeiner. Synthesis of asynchronous systems. In 16th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2006), pages 127-142. Springer Verlag, 2006.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[She et al., 2006]
Zhikun She, Bican Xia, and Rong Xiao. A semi-algebraic approach for the computation of lyapunov functions. In The IASTED International Conference on Computational Intelligence, 2006.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted

[Smaus, 2006]
Jan-Georg Smaus. Representing Boolean functions as linear pseudo-Boolean constraints. In Youssef Hamadi, editor, Proceedings of the CP 2006 Workshop on the Integration of SAT and CP techniques, 2006.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PDF
open

[Sofronie-Stokkermans, 2006a]
Viorica Sofronie-Stokkermans. Interpolation in local theory extensions. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning: Third International Joint Conference, IJCAR 2006, volume 4130 of Lecture Notes in Artificial Intelligence, pages 235-250, Seattle, USA, 2006. Springer.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Sofronie-Stokkermans, 2006b]
Viorica Sofronie-Stokkermans. Local reasoning in verification. In Proceedings of the Verification Workshop VERIFY'06, pages 128-145, 2006.
Abstract (click to open/close)

Subproject(s): R1,H3

Bibtex

PDF
open

[Thesing, 2006]
Stephan Thesing. Modeling a system controller for timing analysis. In EMSOFT '06: Proceedings of the 6th ACM & IEEE International conference on Embedded software, pages 292-300, New York, NY, USA, 2006. ACM Press.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
restricted

[Toben and Westphal, 2006a]
Tobe Toben and Bernd Westphal. Concurrent LSC verification. In Ranko Lazic and Rajagopal Nagarajan, editors, Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS'05), volume 145 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 95-111, Warwick, UK, January 2006. Elsevier B. V.
Subproject(s): S2

Bibtex

PDF
restricted

[Toben and Westphal, 2006b]
Tobe Toben and Bernd Westphal. On the expressive power of Live Sequence Charts. In Jirí Wiedermann, Gerard Tel, Jaroslav Pokorny, Mária Bieliková, and Július Stuller, editors, Proceedings of the 32nd Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'06), volume 2, pages 33-43, Merín, Czech Republic, January 2006. Institute of Computer Science AS CR, Prague.
Subproject(s): S2

Bibtex

PDF
restricted

[Wehrheim, 2006]
Heike Wehrheim. Incremental Slicing. In Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006, Proceedings, volume 4260 of LNCS, pages 514-528. Springer, 2006.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Westphal and Toben, 2006]
Bernd Westphal and Tobe Toben. The Good, the Bad and the Ugly: Well-formedness of Life Sequence Charts. In Luciano Baresi and R. Heckel, editors, Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering (FASE 2006), LNCS 3922, pages 230-246, Vienna, Austria, March 2006. Springer.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wies et al., 2006]
Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard. Field constraint analysis. In E. Allen Emerson and Kedar S. Namjoshi, editors, Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006), volume 3855 of Lecture Notes in Computer Science, pages 157-173, Charleston, SC, USA, January 2006. Springer.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wimmer et al., 2006a]
Ralf Wimmer, Marc Herbstritt, and Bernd Becker. Minimization of large state spaces using symbolic branching bisimulation. In Proceedings of the IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS), Prague, April 2006.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Wimmer et al., 2006b]
Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, and Bernd Becker. Sigref -- a symbolic bisimulation tool box. In Susanne Graf and Wenhui Zhang, editors, 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 4218 of Lecture Notes in Computer Science, pages 477-492, Beijing, China, October 2006. Springer-Verlag.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wolovick and Johr, 2006]
Nicolás Wolovick and Sven Johr. A characterization of meaningful schedulers for continuous-time markov decision processes. In Eugene Asarin and Patricia Bouyer, editors, Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris (France), volume 4202 of Lecture Notes in Computer Science, pages 352-367. Springer-Verlag, 2006.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Ábrahám et al., 2005a]
Erika Ábrahám, Bernd Becker, Felix Klaedtke, and Martin Steffen. Optimizing bounded model checking for linear hybrid systems. In Proceedings of VMCAI'05 (Verification, Model Checking, and Abstraction), volume 3385 of Lecture Notes in Computer Science, pages 396-412, Paris, January 2005. Springer-Verlag. An extended version of this paper appeared as ATR 4.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Ábrahám et al., 2005b]
Erika Ábrahám, Bernd Becker, Felix Klaedtke, and Martin Steffen. Optimizing bounded model checking for linear hybrid systems: Theory and experimental results. AVACS Technical Report No.  4, SFB/TR 14 AVACS, May 2005. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PDF
open

[Aljazzar et al., 2005]
Husain Aljazzar, Holger Hermanns, and Stefan Leue. Counterexamples for timed probabilistic reachability. In Paul Pettersson and Wang Yi, editors, Formal Modeling and Analysis of Timed Systems, 3th International Conference, FORMATS 2005, Uppsala (Sweden), volume 3829 of Lecture Notes in Computer Science, pages 177-195. Springer-Verlag, 2005.
Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Baier et al., 2005a]
C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking meets performance evaluation. ACM Performance Evaluation Review, 32(4):10-15, 2005.
Subproject(s): S3

Bibtex

PDF
restricted

[Baier et al., 2005b]
C. Baier, H. Hermanns, J.-P. Katoen, and V. Wolf. Comparative branching-time semantics for markov chains. Information and Computation, 200(2):149-214, 2005.
Subproject(s): S3

Bibtex

PDF
restricted

[Baier et al., 2005c]
Christel Baier, Holger Hermanns, Joost-Pieter Katoen, and Boudewijn R. Haverkort. Efficient computation of time-bounded reachability probabilities in uniform continuous-time markov decision processes. Theoretical Computer Science, 345(1):2-26, 2005.
Subproject(s): S3

Bibtex

PDF
restricted

[Becker et al., 2005]
Bernd Becker, Markus Behle, Friedrich Eisenbrand, and Ralf Wimmer. Bdds in a branch and cut framework. In Sotiris Nikoletseas, editor, Experimental and Efficient Algorithms, Proceedings of the 4th International Workshop on Efficient and Experimental Algorithms (WEA 05), volume 3503 of Lecture Notes in Computer Science, pages 452-463, Santorini, Greece, May 2005. Springer.
Abstract (click to open/close)

Subproject(s): H2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Brückner, 2005]
Ingo Brückner. Slicing CSP-OZ specifications for verification. Poster Session, 4th International Conference of B and Z Users (ZB '05), 2005.
Subproject(s): R1

Bibtex

PDF
open

[Brückner and Metzler, 2005]
I. Brückner and B. Metzler. Deductive verification for improving slicing of integrated formal specifications. In Proceedings of the 17th Nordic Workshop on Programming Theory, pages 39-41. University of Copenhagen, Denmark, October 2005.
Subproject(s): R1

Bibtex

PDF
restricted

[Brückner and Wehrheim, 2005a]
I. Brückner and H. Wehrheim. Slicing an integrated formal method for verification. In ICFEM 2005: Seventh International Conference on Formal Engineering Methods, volume 3785 of LNCS, pages 360-374. Springer, 2005.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Brückner and Wehrheim, 2005b]
I. Brückner and H. Wehrheim. Slicing CSP-OZ specifications for verification. AVACS Technical Report No.  7, SFB/TR 14 AVACS, November 2005. ISSN: 1860-9821, http://www.avacs.org. This is the full version of [Br{ü}ckner and Wehrheim, 2005a].
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Brückner and Wehrheim, 2005c]
I. Brückner and H. Wehrheim. Slicing Object-Z specifications for verification. AVACS Technical Report No.  3, SFB/TR 14 AVACS, April 2005. ISSN: 1860-9821, http://www.avacs.org. This is the full version of [Br{ü}ckner and Wehrheim, 2005d].
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Brückner and Wehrheim, 2005d]
I. Brückner and H. Wehrheim. Slicing Object-Z specifications for verification. In ZB 2005: 4th International Conference of B and Z Users, number 3455 in LNCS, pages 415-434. Springer, 2005.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Burchardt et al., 2005a]
Henning Burchardt, Jens Oehlerking, and Oliver Theel. The role of state-space partitioning in automated verification of affine hybrid system stability. In Proceedings of the 3rd International Conference on Computing, Communications and Control Technologies, volume 1, pages 187-192. International Institute of Informatics and Systemics, 2005.
Abstract (click to open/close)

Keywords: stability, hybrid systems, Lyapunov functions, piecewise affine systems, linear matrix inequalities, partitioning
Subproject(s): H4

Bibtex

PDF
restricted

[Burchardt et al., 2005b]
Henning Burchardt, Jens Oehlerking, and Oliver Theel. Towards push-of-a-button stability verification for discrete-time hybrid systems. In 11th Pacific Rim International Symposium on Dependable Computing, 2005.
Abstract (click to open/close)

Subproject(s): H3,H4

Bibtex

PDF
restricted

[Cloth et al., 2005]
Lucia Cloth, Joost-Pieter Katoen, Maneesh Khattri, and Reza Pulungan. Model checking markov reward models with impulse rewards. In International Conference on Dependable Systems and Networks (DSN'05), pages 722-731, 2005.
Subproject(s): S3

Bibtex

PDF
restricted

[Damm and Westphal, 2005]
Werner Damm and Bernd Westphal. Live and let die: LSC-based verification of UML-models. Science of Computer Programming, 55(1-3):117-159, März 2005.
Subproject(s): S2

Bibtex

PDF
restricted

[Damm et al., 2005a]
Werner Damm, Bernhard Josko, Amir Pnueli, and Angelika Votintseva. A discrete-time UML semantics for concurrency and communication in safety-critical applications. Science of Computer Programming, 55(1-3):81-115, March 2005.
Subproject(s): S2

Bibtex

PDF
restricted

[Damm et al., 2005b]
Werner Damm, Guilherme Pinto, and Stefan Ratschan. Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. In Doron A. Peled and Yih-Kuen Tsay, editors, Proceedings of the Third International Symposium on Automated Technology for Verification and Analysis, number 3707 in LNCS. Springer, 2005.
Abstract (click to open/close)

Subproject(s): H3,H4

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Dierks, 2005a]
H. Dierks. Finding Optimal Plans for Domains with Continuous Effects with UPPAAL CORA. In Proceedings of the ICAPS'05 Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems, 2005.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open

[Dierks, 2005b]
H. Dierks. Heuristic Guided Model-Checking of Real-Time Systems. Technical report, University of Oldenburg, Department of Computer Science, Oldenburg, Germany, 2005. full version of [Dierks, 2004b].
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open

[Dierks, 2005c]
H. Dierks. Time, Abstraction and Heuristics -- Automatic Verification and Planning of Timed Systems using Abstraction and Heuristics. Habilitation thesis, July 2005.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open

[Eggers, 2005]
Andreas Eggers. Induktive Verifikation linearer Hybrider Systeme. BSc thesis, Carl von Ossietzky Universität Oldenburg, Department für Informatik, 2005.
Abstract (click to open/close)

Subproject(s): H1,H2

Bibtex

PDF
open

[Enslev et al., 2005]
Jacob Enslev, Anne-Sofie Nielsen, Martin Fränzle, and Michael R. Hansen. Bounded model construction for duration calculus. In Neil Jones et al., editor, Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05). Københavns Universitet, October 2005.
Subproject(s): H1

Bibtex

PDF
restricted

[Faber, 2005]
J. Faber. Verifying real-time aspects of the European Train Control System. In Proceedings of the 17th Nordic Workshop on Programming Theory, pages 67-70. University of Copenhagen, Denmark, October 2005.
Subproject(s): R1

Bibtex

PDF
restricted

[Finkbeiner and Schewe, 2005a]
Bernd Finkbeiner and Sven Schewe. Semi-automatic distributed synthesis. In 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA 2005), volume 3707 of Lecture Notes in Computer Science, pages 263-277. Springer Verlag, October 2005.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Finkbeiner and Schewe, 2005b]
Bernd Finkbeiner and Sven Schewe. Uniform distributed synthesis. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), pages 321-330. IEEE Computer Society Press, June 2005.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PostScript
restricted

PDF
restricted

[Fränzle and Hansen, 2005]
Martin Fränzle and Michael R. Hansen. A robust interpretation of duration calculus. In Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC 05), volume 3722 of LNCS, pages 257-271. Springer Verlag, 2005.
Abstract (click to open/close)

Keywords: Metric-time temporal logic; Robust interpretation; Discrete time vs. dense time
Subproject(s): H1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Herbstritt and Becker, 2005]
Marc Herbstritt and Bernd Becker. On SAT-based Bounded Invariant Checking of Blackbox Designs. In Proc. of Microprocessor Test and Verification Workshop (MTV), pages 23-28, Austin (TX), USA, 2005. IEEE Computer Society.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Hermanns et al., 2005a]
H. Hermanns, D.N. Jansen, and Y.S. Usenko. From stocharts to modest: a comparative reliability analysis of train radio communications. In 5th International Workshop on Software and Performance, WOSP 2005, pages 13-23. ACM Press, 2005.
Subproject(s): S3

Bibtex

PDF
restricted

[Hermanns et al., 2005b]
Holger Hermanns, David N. Jansen, and Yaroslav S. Usenko. A comparative reliability analysis of ETCS train radio communications. AVACS Technical Report No.  2, SFB/TR 14 AVACS, February 2005. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Keywords: UML, stochastic systems, concurrency, tool support, reliability, wireless communication, European Train Control System (ETCS)
Subproject(s): S3

Bibtex

PDF
open

[Hoenicke and Maier, 2005a]
Jochen Hoenicke and Patrick Maier. Model-checking of specifications integrating processes, data and time. AVACS Technical Report No.  5, SFB/TR 14 AVACS, May 2005. ISSN: 1860-9821, http://www.avacs.org. This is an extended version of [Hoenicke and Maier, 2005b].
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Hoenicke and Maier, 2005b]
Jochen Hoenicke and Patrick Maier. Model-checking of specifications integrating processes, data and time. In J.S. Fitzgerald, I.J. Hayes, and A. Tarlecki, editors, FM 2005, volume 3582 of LNCS, pages 465-480. Springer, 2005. An extended version of this paper appeared as AVACS Technical Report No. 5.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Hoffmann, 2005]
Jörg Hoffmann. Where `ignoring delete lists' works: Local search topology in planning benchmarks. Journal of Artificial Intelligence Research, 24:685-758, 2005.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open

[Jacobs and Waldmann, 2005]
Swen Jacobs and Uwe Waldmann. Comparing Instance Generation Methods for Automated Reasoning. In Bernhard Beckert, editor, Proc.of TABLEAUX 2005, LNAI 3702, pages 153-168. Springer, 2005.
Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Jansen and H.Hermanns, 2005]
D.N. Jansen and H.Hermanns. Qos modelling and analysis with uml-statecharts: The stocharts approach. ACM Performance Evaluation Review, 32(4):28-33, 2005.
Subproject(s): S3

Bibtex

PDF
restricted

[Johannes et al., 2005]
Dierk Johannes, Raimund Seidel, and Reinhard Wilhelm. Algorithm animation using shape analysis: visualising abstract executions. In SoftVis '05: Proceedings of the 2005 ACM symposium on Software visualization, pages 17-26, New York, NY, USA, 2005. ACM Press.
Subproject(s): S2

Bibtex

PDF
restricted

[Johr, 2005]
S. Johr. Transforming stochastic activity networks to continuous-time markov decision processes. In Proceedings of the PMCCS-7, September 2005.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted

[Lohrey et al., 2005]
M. Lohrey, P.R. D'Argenio, and H.Hermanns. Axiomatising divergence. Information and Computation, 203(2):115-238, 2005.
Subproject(s): S3

Bibtex

PDF
restricted

[Maurer, 2005]
Tobias Maurer. Distributed games for reactive systems. Diploma thesis, Universität des Saarlandes, Germany, October 2005.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Metzner, 2005]
Alexander Metzner. Predictable and efficient architectures for real-time system synthesis. In Proceedings of the Workshop on Embedded Real-Time Systems Implementation, 2005.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Metzner and Herde, 2005]
Alexander Metzner and Christian Herde. RTSAT - Scheduling Tasks in Distributed Real-Time Systems by Enhanced Satisifiability Checking. In Proceedings of the IEEE Real-Time Systems Symposium, Work in Progress Session, 2005.
Abstract (click to open/close)

Subproject(s): R2,H2

Bibtex

PDF
open

[Metzner et al., 2005]
A. Metzner, M. Fränzle, C. Herde, and I. Stierand. Scheduling Distributed Real-Time Systems by Satisfiability Checking. In Proceedings of the IEEE Conference on Embedded and Real-Time Computing Systems and Applications, pages 409-415. IEEE Computer Society, 2005.
Abstract (click to open/close)

Subproject(s): R2,H2

Bibtex

PDF
restricted

[Meyer, 2005]
R. Meyer. Model-Checking von Phasen-Event-Automaten bezüglich Duration Calculus Formeln mittels Testautomaten. Master's thesis, University of Oldenburg, 2005.
Abstract (click to open/close)

Subproject(s): R1

Bibtex

PDF
open

[Nopper and Scholl, 2005]
T. Nopper and C. Scholl. Flexible modeling of unknowns in model checking for incomplete designs. In GI/ITG/GMM Workshop, 2005.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Oehlerking et al., 2005a]
Jens Oehlerking, Henning Burchardt, and Oliver Theel. Towards automatic verification of affine hybrid system stability. SIGBED Review, Special Issue on IEEE RTAS 2005 Work-in-Progress, 2:27 -- 30, 2005.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted

[Oehlerking et al., 2005b]
Jens Oehlerking, Abhishek Dhama, and Oliver Theel. Towards automatic convergence verification of self-stabilizing algorithms. In Sébastien Tixeuil and Ted Herman, editors, Symposium on Self-Stabilization, Lecture Notes in Computer Science 3764, pages 198 -- 213. Springer, 2005.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Olderog and Wehrheim, 2005]
Ernst-Rüdiger Olderog and Heike Wehrheim. Specification and (property) inheritance in csp-oz. Science of Computer Programming, 55:227-257, 2005.
Subproject(s): R1

Bibtex

PDF
restricted

[Peter, 2005]
Hans-Jörg Peter. Controller program synthesis for industrial machines. Diploma thesis, Universität des Saarlandes, Germany, November 2005.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Pnueli et al., 2005]
Amir Pnueli, Andreas Podelski, and Andrey Rybalchenko. Separating fairness and well-foundedness for the analysis of fair discrete systems. In TACAS'2005: 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 3440 of LNCS, pages 124-139. Springer, 2005.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Podelski and Rybalchenko, 2005]
Andreas Podelski and Andrey Rybalchenko. Transition predicate abstraction and fair termination. In POPL'2005, 2005.
Abstract (click to open/close)

Subproject(s): R1,H4

Bibtex

PDF
open

[Podelski and Schaefer, 2005]
Andreas Podelski and Ina Schaefer. Local Reasoning for Termination. In Proceedings of the 1st international Workshop on the verification of COncurrent Systems with dynaMIC Allocated Heaps (COSMICAH 2005), Lisboa, Portugal, July 2005.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
open

[Podelski and Wies, 2005]
Andreas Podelski and Thomas Wies. Boolean heaps. In Chris Hankin and Igor Siveroni, editors, Proceedings of the 12th International Static Analysis Symposium (SAS 2005), volume 3672 of Lecture Notes in Computer Science, pages 268-283, London, UK, September 2005. Springer.
Abstract (click to open/close)

Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Podelski et al., 2005]
Andreas Podelski, Ina Schaefer, and Silke Wagner. Summaries for while programs with recursion. In Proc. ESOP 2005, volume 3444 of Lecture Notes in Computer Science, pages 94-107. Springer Verlag, 2005.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Ratschan, 2005]
Stefan Ratschan. Solving undecidable problems in the theory of real numbers and hybrid systems. In A. Dolzmann, A. Seidl, and T. Sturm, editors, Algorithmic Algebra and Logic 2005, Proceedings of the Conference in Honor of the 60th Birthday of Volker Weispfenning, pages 213-216. Books on Demand GmbH, 2005.
Abstract (click to open/close)

Subproject(s): H1

Bibtex

PDF
restricted

[Ratschan and She, 2005]
Stefan Ratschan and Zhikun She. Safety verification of hybrid systems by constraint propagation based abstraction refinement. In Manfred Morari and Lothar Thiele, editors, Hybrid Systems: Computation and Control, volume 3414 of LNCS. Springer, 2005.
Subproject(s): H1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Regenberg, 2005]
Jens Regenberg. Synthesis of reactive systems. Diploma thesis, Universität des Saarlandes, Germany, December 2005.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
open

[Rinetzky et al., 2005]
Noam Rinetzky, Jörg Bauer, Thomas W. Reps, Shmuel Sagiv, and Reinhard Wilhelm. A semantics for procedure local heaps and its abstractions.. In Jens Palsberg and Martín Abadi, editors, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 296-309. ACM Press, 2005.
Subproject(s): S2

Bibtex

PDF
restricted

[Rybalchenko et al., 2005]
Andrey Rybalchenko, Byron Cook, and Andreas Podelski. Abstraction-refinement for termination. In SAS 2005, 2005.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
open

[Sofronie-Stokkermans, 2005]
Viorica Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions. In Robert Nieuwenhuis, editor, 20th International Conference on Automated Deduction (CADE-20), volume 3632 of Lecture Notes in Artificial Intelligence, pages 219-234, Tallinn, Estonia, 2005. Springer.
Subproject(s): R1,H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Swaminathan and Fränzle, 2005]
Mani Swaminathan and Martin Fränzle. Automatic and scalable verification of robust real-time systems. In Neil Jones et al., editor, Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05). Københavns Universitet, October 2005.
Subproject(s): H1

Bibtex

PDF
restricted

[Wehrheim, 2005]
Heike Wehrheim. Slicing techniques for verification re-use. Theoretical Computer Science, 343(3):509-528, 2005.
Subproject(s): R1

Bibtex

PDF
restricted

[Westphal, 2005]
Bernd Westphal. LSC verification for UML models with unbounded creation and destruction. In Willem Visser Byron Cook, Scott Stoller, editor, SoftMC 2005, Workshop on Software Model Checking (Satellite Workshop of CAV '05), ENTCS. Elsevier B.V., July 2005.
Subproject(s): S2

Bibtex

PDF
restricted

[Wilhelm, 2005a]
Reinhard Wilhelm. Determining bounds on execution times. In R. Zurawski, editor, Handbook on Embedded Systems, pages 14-1,14-23. CRC Press, 2005.
Subproject(s): R2

Bibtex

PDF
restricted

[Wilhelm, 2005b]
Reinhard Wilhelm. Timing analysis and timing predictability. In F.S. de Boer et al., editor, FMCO 2004, volume 3657 of LNCS, pages 317 -- 323. Springer Verlag, 2005.
Subproject(s): R2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Zhang et al., 2005a]
Lijun Zhang, Holger Hermanns, and David N. Jansen. Logic and model checking for hidden markov models. AVACS Technical Report No.  6, SFB/TR 14 AVACS, July 2005. ISSN: 1860-9821, http://www.avacs.org. This report is the full version of a paper which appeared in FORTE'05  [Zhang et al., 2005b].
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
open

[Zhang et al., 2005b]
Lijun Zhang, Holger Hermanns, and David N. Jansen. Logic and model checking for hidden markov models. In Farn Wang, editor, Formal techniques for networked and distributed systems, FORTE, volume 3731 of Lecture notes in computer science, pages 98-112, Berlin, 2005. Springer.
Abstract (click to open/close)

Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Baier et al., 2004a]
C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Efficient computation of time-bounded reachability probabilities in uniform continuous-time markov decision processes. In 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, number 2988 in Lecture Notes in Computer Science, pages 61-76. Springer-Verlag, 2004.
Subproject(s): S3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Baier et al., 2004b]
C. Baier, B. Haverkort, H. Hermanns, J.-P.Katoen, and M. Siegle, editors. Validation of Stochastic Systems. Number 2925 in Lecture Notes in Computer Science. Springer-Verlag, 2004.
Subproject(s): S3

Bibtex
© Springer Verlag (see article at SpringerLink)

[Baier et al., 2004c]
C. Baier, H. Hermanns, J.-P. Katoen, and V. Wolf. Probabilistic weak simulation is decidable in polynominal time. Information Processing Letters, 89(3):123-130, 2004.
Subproject(s): S3

Bibtex

PDF
restricted

[Becker et al., 2004]
Bernd Becker, Markus Behle, Fritz Eisenbrand, Martin Fränzle, Marc Herbstritt, Christian Herde, Joerg Hoffmann, Daniel Kröning, Bernhard Nebel, Ilia Polian, and Ralf Wimmer. Bounded model checking and inductive verification of hybrid discrete-continuous systems. In ITG/GI/GMM-Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', 2004.
Abstract (click to open/close)

Keywords: Hybrid System Verification, Bounded Model Checking, Inductive Verification, Verification Engines
Subproject(s): H2

Bibtex

PDF
restricted

[Bohnenkamp et al., 2004]
H.C. Bohnenkamp, H. Hermanns, A. Mader, R. Klaren, and Y.S. Usenko. Synthesis and stochastic assessment of schedules for lacquer production. In 1st International Conference on Quantitative Evaluation of Systems, QEST 2004, pages 28-37. IEEE CS Press, 2004.
Subproject(s): S3

Bibtex

PDF
restricted

[Brill et al., 2004a]
Matthias Brill, Ralf Buschermöhle, Werner Damm, Jochen Klose, Bernd Westphal, and Hartmut Wittke. Formal verification of LSCs in the development process. In Hartmut Ehrig, Werner Damm, Jörg Desel, Martin Große-Rhode, Wolfgang Reif, Eckehard Schnieder, and Engelbert Westkämper, editors, Integration of Software Specification Techniques for Applications in Engineering, number 3147 in Lecture Notes in Computer Science, pages 494-516. Springer-Verlag, 2004.
Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Brill et al., 2004b]
Matthias Brill, Werner Damm, Jochen Klose, Bernd Westphal, and Hartmut Wittke. Live Sequence Charts. In Hartmut Ehrig, Werner Damm, Jörg Desel, Martin Große-Rhode, Wolfgang Reif, Eckehard Schnieder, and Engelbert Westkämper, editors, Integration of Software Specification Techniques for Applications in Engineering, number 3147 in Lecture Notes in Computer Science, pages 374-399. Springer-Verlag, 2004.
Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Brückner, 2004]
I. Brückner. Slicing CSP-OZ Specifications. In P. Pettersson and W. Yi, editors, Proceedings of the 16th Nordic Workshop on Programming Theory, number 2004-041 in Technical Reports of the Department of Information Technology, pages 71-73. Uppsala University, Sweden, October 2004.
Subproject(s): R1

Bibtex

PDF
restricted

[Damm et al., 2004]
W. Damm, H. Hungar, and E.-R. Olderog. On the verification of cooperating traffic agents. In F.S. de Boer, M.M. Bonsangue, S. Graf, and W.-P. de Roever, editors, Proc.FMCO '03: Formal Methods for Components and Objects, LNCS 3188, pages 78-110, 2004.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Dierks, 2004a]
H. Dierks. Comparing model-checking and logical reasoning for real-time systems. Formal Aspects of Computing, 16(2):104-120, May 2004.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open

[Dierks, 2004b]
H. Dierks. Heuristic Guided Model-Checking of Real-Time Systems (Extended Abstract). In P. Pettersson and Wang Yi, editors, Proceedings of the 16th Nordic Workshop on Programming Theory, Technical Report 2004-041, pages 14-16. Uppsala University, Sweden, October 2004.
Abstract (click to open/close)

Subproject(s): R3

Bibtex

PDF
open

[Fränzle, 2004]
Martin Fränzle. Model-checking dense-time duration calculus. Formal Aspects of Computing Science, 16(2):121-139, 2004.
Subproject(s): H1

Bibtex

PDF
restricted

[Fränzle and Hansen, 2004]
Martin Fränzle and Michael R. Hansen. A robust interpretation of duration calculus. In Paul Pettersson and Wang Yi, editors, Proceedings of the 16th Nordic Workshop on Programming Theory (NWPT 04),, pages 83-85. Dept. of Information Technology, Uppsala University, 2004.
Subproject(s): H1

Bibtex

PDF
restricted

[Fränzle and Herde, 2004]
Martin Fränzle and Christian Herde. Efficient proof engines for bounded model checking of hybrid systems. In Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 04), Electronic Notes in Theoretical Computer Science (ENTCS). Elsevier, 2004.
Abstract (click to open/close)

Keywords: verification, bounded model checking, hybrid systems, infinite-state systems, decision procedures, satisfiability
Subproject(s): H2

Bibtex

PDF
restricted

[Ganzinger et al., 2004a]
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): Fast decision procedures. In R. Alur and D. Peled, editors, 16th International Conference on Computer Aided Verification, CAV'04, volume 3114 of Lecture Notes in Computer Science, pages 175-188, Boston, MA, USA, 2004. Springer.
Abstract (click to open/close)

Subproject(s): H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Ganzinger et al., 2004b]
Harald Ganzinger, Viorica Sofronie-Stokkermans, and Uwe Waldmann. Modular proof systems for partial functions with weak equality. In David Basin and Michael Rusinowitch, editors, Automated reasoning : Second International Joint Conference, IJCAR 2004, volume 3097 of Lecture Notes in Artificial Intelligence, pages 168-182, Cork, Ireland, June 2004. Springer.
Subproject(s): R1,H3

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Helmert, 2004]
Malte Helmert. A planning heuristic based on causal graph analysis. In Shlomo Zilberstein, Jana Koehler, and Sven Koenig, editors, Fourteenth International Conference on Automated Planning and Scheduling (ICAPS 2004), pages 161-170, Menlo Park, California, 2004. AAAI Press.
Subproject(s): S1

Bibtex

PDF
restricted

[Hermanns, 2004]
Holger Hermanns. Construction and verification of concurrent performance and reliability models. In G. Paun, G. Rozenberg, and A. Salomoa, editors, Current Trends in Theoretical Computer Science, volume 2 of Current Trends in Theoretical Computer Science, chapter 3, pages 351-377. World Scientific, 2004.
Subproject(s): S3

Bibtex

[Jansen and Hermanns, 2004]
D.N. Jansen and H. Hermanns. Dependability checking with stocharts: Is train radio reliable enough for trains?. In 1st International Conference on Quantitative Evaluation of Systems, QEST 2004, pages 250-259. IEEE CS Press, 2004.
Subproject(s): S3

Bibtex

PDF
restricted

[Klaedtke, 2004a]
Felix Klaedtke. On the automata size for Presburger arithmetic. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pages 110-119. IEEE Computer Society Press, 2004. An extended version of this paper is [Klaedtke, 2004b].
Abstract (click to open/close)

Keywords: Presburger arithmetic, automata constructions, automata size, upper and lower bounds
Subproject(s): H1

Bibtex

PostScript
restricted

PDF
restricted

[Klaedtke, 2004b]
Felix Klaedtke. On the automata size for Presburger arithmetic. Extended version of [Klaedtke, 2004a], 2004.
Abstract (click to open/close)

Keywords: Presburger arithmetic, automata constructions, automata size, upper and lower bounds
Subproject(s): H1

Bibtex

PostScript
open

PDF
open

[Metzner, 2004]
Alexander Metzner. Why model-checking can improve WCET analysis. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV04), LNCS 3114, pages 334-347, 2004.
Abstract (click to open/close)

Keywords: Model Checking, WCET Analysis
Subproject(s): R2

Bibtex

PostScript
restricted

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Nopper and Scholl, 2004a]
T. Nopper and C. Scholl. Approximate symbolic model checking for incomplete designs. In Formal Methods in Computer-Aided Design, pages 290-305, Nov 2004.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Nopper and Scholl, 2004b]
T. Nopper and C. Scholl. Approximate symbolic model checking of incomplete designs. In Int'l Workshop on Logic and Synthesis, pages 377-384, Jun 2004.
Abstract (click to open/close)

Subproject(s): S1

Bibtex

PDF
restricted

[Nopper and Scholl, 2004c]
T. Nopper and C. Scholl. Symbolic model checking of incomplete designs. Technical Report 201, Albert-Ludwigs-University, Jun 2004.
Subproject(s): S1

Bibtex

PDF
open

[Podelski and Rybalchenko, 2004a]
Andreas Podelski and Andrey Rybalchenko. Transition invariants. In 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pages 32-41. IEEE Computer Society, 2004. Draft version available as [Podelski and Rybalchenko, 2004b].
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PDF
open

[Podelski and Rybalchenko, 2004b]
Andreas Podelski and Andrey Rybalchenko. Transition invariants. Draft version of [Podelski and Rybalchenko, 2004a], 2004.
Abstract (click to open/close)

Subproject(s): H4

Bibtex

PostScript
open

PDF
open

[Rakib et al., 2004]
Abdur Rakib, Oleg Parshin, Stephan Thesing, and Reinhard Wilhelm. Component-wise instruction-cache behavior prediction. In ATVA 2004, volume 3299 of LNCS, pages 211-229, 2004.
Subproject(s): R2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Reps et al., 2004]
Thomas W. Reps, Shmuel Sagiv, and Reinhard Wilhelm. Static program analysis via 3-valued logic. In CAV 2004, volume 3114 of LNCS, pages 15-30, 2004.
Subproject(s): S2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Rinetzky et al., 2004]
Noam Rinetzky, Jörg Bauer, Thomas Reps, Mooly Sagiv, and Reinhard Wilhelm. A semantics for procedure local heaps and its abstraction. AVACS Technical Report No.  1, SFB/TR 14 AVACS, Oktober 2004. ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close)

Subproject(s): R2

Bibtex

PDF
open

[Scholl and Büche, 2004]
C. Scholl and M. Büche. Filter based diagnosis for multiple design errors. In GI/ITG/GMM-Workshop `Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen', 2004.
Subproject(s): S1

Bibtex

[Thiele and Wilhelm, 2004]
Lothar Thiele and Reinhard Wilhelm. Design for timing predictability. Real-Time Systems, 28:157 -- 177, 2004.
Subproject(s): R2

Bibtex

PDF
restricted

[Wehrheim, 2004]
Heike Wehrheim. Preserving properties under change. In FMCO 2003: Formal Methods for Components and Objects, number 3188 in LNCS, pages 330-343. Springer, 2004.
Subproject(s): R1

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wilhelm, 2004a]
Reinhard Wilhelm. Formal analysis of processor timing models. In Susanne Graf and Laurent Mounier, editors, Model Checking Software, 11th International SPIN Workshop, volume 2989 of Lecture Notes in Computer Science, pages 1-4. Springer, 2004.
Subproject(s): R2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Wilhelm, 2004b]
Reinhard Wilhelm. Why AI + ILP is good for WCET, but MC is not, nor ILP alone. In VMCAI 2004, volume 2937 of LNCS, pages 309-322, 2004.
Subproject(s): R2

Bibtex

PDF
restricted
© Springer Verlag (see article at SpringerLink)

[Zhang, 2004]
Lijun Zhang. Logic and model checking for hidden markov models. Master's thesis, Universitaet des Saarlandes, Saarbruecken (Germany), 2004.
Subproject(s): S3

Bibtex

[Fränzle et al.]
Martin Fränzle, Tino Teige, and Andreas Eggers. Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. The Journal of Logic and Algebraic Programming. to appear.
Abstract (click to open/close)

Keywords: Probabilistic hybrid automata, bounded model checking, arithmetic constraint solving, stochastic satisfiability
Subproject(s): H1/2,H4

Bibtex

PDF
restricted

[Teige et al.]
Tino Teige, Andreas Eggers, and Martin Fränzle. Constraint-based analysis of concurrent probabilistic hybrid systems: An application to networked automation systems. Nonlinear Analysis: Hybrid Systems. to appear.
Abstract (click to open/close)

Keywords: Concurrent probabilistic hybrid systems, probabilistic logic, constraint satisfaction problems, problem solvers, automatic verification
Subproject(s): H1/2,H4

Bibtex

PDF
restricted