| Titel | Autor(en) | Quelle |
|---|---|---|
| Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFS-FIFO | Alfons Laarman, David Faragó |
Proceedings of the 5th NASA Formal Methods Symposium (NFM 2013), NASA Ames Research Center, CA, USA, May 14-16, 2013. LNCS, Springer, 2013. |
| Titel | Autor(en) | Quelle |
|---|---|---|
| A Proof Assistant for Alloy Specifications | Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri |
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012 |
| Titel | Autor(en) | Quelle |
|---|---|---|
| A Dual-Engine for Early Analysis of Critical Systems | Aboubakr Achraf El Ghazi, Ulrich Geilmann, Mattias Ulbrich, Mana Taghdiri |
Dependable Software for Critical Infrastructures (DSCI), 2011 |
| Predicate Abstraction in a Program Logic Calculus | Science of Computer Programming 76 (10), Elsevier, 2011 |
|
| The 1st Verified Software Competition: Experience Report | Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß |
17th International Symposium on Formal Methods (FM 2011), Limerick, Ireland. LNCS 6664, Springer, 2011. Best paper award at FM 2011. |
| Nondeterministic Coverage Metrics as Key Performance Indicator for Model- and Value-based Testing | 31. Treffen der GI-Fachgruppe Test, Analyse & Verifikation von Software (TAV), am 3. und 4. Februar 2011 in Paderborn. Testing in modern IT-Contexts, ROI und KPIs des Testens. |
|
| Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction | PhD thesis, Karlsruhe Institute of Technology. KIT Scientific Publishing, 2011 |
|
| A Dynamic Logic for Unstructured Programs with Embedded Assertions | International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France. LNCS 6528, Springer, 2011 |
|
| Dynamic Frames in Java Dynamic Logic | International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France. LNCS 6528, Springer, 2011 |
| Titel | Autor(en) | Quelle |
|---|---|---|
| Correctness of Sensor Network Applications by Software Bounded Model Checking | Formal Methods for Industrial Critical Systems - 15th International Workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010. LNCS 6371, Springer, 2010. |
|
| Improved Underspecification for Model-based Testing in Agile Development | Lecture Notes in Informatics (LNI) Volume P-179 - Proceedings of the Second International Workshop on Formal Methods and Agile Methods, 17 September 2010, Pisa (Italy). |
|
| Coverage Criteria for Nondeterministic Systems | testing experience, The Magazine for Professional Testers; 3/2010: Metrics, pages 104-106; Díaz & Hilterscheid, September 2010; ISSN 1866-5705. |
|
| On the Semantic Relationship between Datalog and Description Logics | Web Reasoning and Rule Systems - Fourth International Conference, RR 2010, Bressanone/Brixen, Italy, September 22-24, 2010. |
|
| Model-based Testing in Agile Software Development | 30. Treffen der GI-Fachgruppe Test, Analyse & Verifikation von Software (TAV), Testing meets Agility. 17.06.2010 |
|
| A Formalization of the RTSJ Scoped Memory Model in Dynamic Logic | ||
| Enhanced Dispatchability of Aircrafts using Multi-Static Configurations | Christian Engel |
Embedded Real Time Software and Systems (ERTS² 2010), Toulouse, France, 2010 |
| Deductive Verification of a Byzantine Agreement Protocol | Roman Krenický |
| Titel | Autor(en) | Quelle |
|---|---|---|
| Improving Non-Progress Cycle Checks | Model Checking Software, 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. LNCS, vol. 5578, pp. 50-67. Springer, Heidelberg (2009). |
|
| Deductive Verification of Safety-Critical Java Programs | ||
| Abstract Interpretation of Symbolic Execution with Explicit State Updates | 7th International Symposium on Formal Methods for Components and Objects (FMCO 2008), Sophia Antipolis, France. LNCS 5751, Springer, 2009 |
|
| Verification of Modifies Clauses in Dynamic Logic with Non-rigid Functions | Technical Report 2009-9, Department of Computer Science, University of Karlsruhe, 2009 |
|
| Predicate Abstraction in a Program Logic Calculus | 7th International Conference on integrated Formal Methods (iFM 2009), Düsseldorf, Germany. LNCS 5423, Springer, 2009 |
| Titel | Autor(en) | Quelle |
|---|---|---|
| Deductive Verification of RTSJ Programs | 2nd Junior Researcher Workshop on Real-Time Computing (JRWRTC 2008), Rennes, France, 2008 |
|
| Specification Predicates with Explicit Dependency Information | 5th International Verification Workshop (VERIFY'08), |
|
| Analysis of authenticated Query Flooding by Probabilistic Means | IEEE/IFIP WONS 2008, |
|
| Integrating Verification and Testing of Object-Oriented Software | Christian Engel |
2nd International Conference on Tests and Proofs, Prato, Italy, 2008 |
| Titel | Autor(en) | Quelle |
|---|---|---|
| Generating Unit Tests from Formal Proofs | International Conference on Tests And Proofs (TAP), ETH Zürich, Switzerland, 2007 |
|
| Inferring Invariants by Symbolic Execution | 4th International Verification Workshop (VERIFY'07), Workshop at CADE-21, Bremen, Germany, 2007 |
|
| KeY: A Formal Method for Object-Oriented Systems | Wolfgang Ahrendt |
Invited Paper, 9th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'07), Paphos, Cyprus. LNCS 4468, Springer, 2007 |
| Model Checking for Energy Efficient Scheduling in Wireless Sensor Networks | GI/ITG KuVS Fachgespräch Aachen 2007 - Energiebewusste Systeme und Methoden |
|
| The KeY System 1.0 (Deduction Component) | Bernhard Beckert |
21st International Conference on Automated Deduction (CADE-21), Bremen, Germany. LNCS 4603, Springer, 2007 |
| Verification of Memory Performance Contracts with KeY | Technischer Bericht, Universität Karlsruhe (TH), 2007 |
|
| Verification of Object-Oriented Software: The KeY Approach | Bernhard Beckert |
LNCS 4334, Springer, 2007 |
| Verifying Object-Oriented Programs with KeY: A Tutorial | Wolfgang Ahrendt |
5th International Symposium on Formal Methods for Components and Objects (FMCO'06), Amsterdam, The Netherlands. LNCS 4709, Springer, 2007 |
| Verifying the Mondex Case Study | 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM'07), London, UK. IEEE Press, 2007 |
|
| Verifying the Mondex Case Study: The KeY Approach | Technical Report 2007-4, Universität Karlsruhe |