| Title | Author | Source |
|---|---|---|
| Computing Specification-Sensitive Abstractions for Program Verification | Tianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl and Mana Taghdiri |
2th Symposium on Dependable Software Engineering Theories, Tools and Applications |
| First-Order Transitive Closure Axiomatization via Iterative Invariant Injections | Aboubakr Achraf El Ghazi, Mana Taghdiri, Mihai Herda |
7th NASA Formal Methods Symposium (NFM), Pasadena, April 2015 |
| On Verifying Relational Specifications of Java Programs with JKelloy | Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, Mana Taghdiri |
Karlsruhe Institute of Technology, Karlsruhe Reports in Informatics, 2014-3, 2014 |
| JKelloy: A Proof Assistant for Relational Specifications of Java Programs | Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, Mana Taghdiri |
6th NASA Formal Methods Symposium (NFM), 2014 |
| Generating JML Specifications from Alloy Expressions |
Daniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri, Shmuel Tyszberowicz |
10th Haifa Verification Conference (HVC), 2014 |
| A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution |
Tianhai Liu, Mateus Araujo, Marcelo d‘Amorim, Mana Taghdiri |
10th Haifa Verification Conference (HVC), 2014 |
| Reducing the Complexity of Quantified Formulas via Variable Elimination | Aboubakr Achraf El Ghazi, Mattias Ulbrich, Mana Taghdiri, Mihai Herda |
11th International Workshop on Satisfiability Modulo Theories (SMT), 2013 |
| Minimizing Models for Tseitin-Encoded SAT Instances | Markus Iser, Carsten Sinz, Mana Taghdiri | 16th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2013 |
| Applications and Extensions of Alloy: Past, Present, and Future | Emina Torlak, Mana Taghdiri, Greg Dennis, Joseph Near |
Mathematical Structures in Computer Science, volume 23, issue 04, pp. 915-933, 2013. |
| Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod (Poster Presentation) | Markus Iser, Mana Taghdiri, Carsten Sinz |
15th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2012 |
| Bounded Program Verification using an SMT Solver: A Case Study | Tianhai Liu, Michael Nagel, Mana Taghdiri |
5th International Conference on Software Testing, Verification and Validation (ICST), 2012 |
| 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 |
| On Proving Alloy Specifications using KeY | Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri |
Karlsruhe Institute of Technology, Technical Report 2011-37, 2011 |
| 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 |
| Relational Reasoning via SMT Solving | Aboubakr Achraf El Ghazi, Mana Taghdiri |
17th International Symposium on Formal Methods (FM), 2011. |
| Information flow analysis via path condition refinement | Mana Taghdiri, Gregor Snelting, Carsten Sinz |
7th International Workshop on Formal Aspects of Security and Trust (FAST), 2010 |
| Analyzing Alloy Formulas using an SMT Solver: A Case Study | Aboubakr Achraf El Ghazi, Mana Taghdiri |
Automated Formal Methods (AFM), 2010 |
| Checking Software Reliability | Mana Taghdiri |
Emerging Research Directions in Computer Science - The Young Informatics Faculty at Karlsruhe Institute of Technology, KIT Scientific Publishing, 2010 |
| Inferring Specifications to Detect Errors in Code | Mana Taghdiri, Daniel Jackson |
Journal of Automated Software Engineering (JASE)– Special issue on selected papers, Volume 14, Issue 1, 2007. (A preliminary version published in ASE’04.) |
| Lightweight Extraction of Syntactic Specifications | Mana Taghdiri, Robert Seater, Daniel Jackson |
International Symposium on Foundations of Software Engineering (FSE), 2006 |
| Inferring Specifications to Detect Errors in Code | Mana Taghdiri |
International Conference on Automated Software Engineering (ASE), 2004. (distinguished paper award) |
| Analyzing Java Programs with F-Soft | Mana Taghdiri, Franjo Ivancic |
NEC Laboratories America, Inc. Technical report TR-2004-L070, 2004 |
| A Lightweight Formal Analysis of a Multicast Key Management Scheme | Mana Taghdiri, Daniel Jackson |
International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), 2003 |
| Debugging Overconstrained Declarative Models Using Unsatisfiable Cores | Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, Mana Taghdiri |
International Conference on Automated Software Engineering (ASE), 2003. (distinguished paper award) |
| Shortest Point-Visible Paths on Polyhedral Surfaces | Ramtin Khosravi, Mohammad Ghodsi, Mana Taghdiri |
International Conference on Computing and Information (ICCI), 2000 |
| Title | Author | Place |
|---|---|---|
| Automatic Program Parallelization | Mana Taghdiri |
Sharif University of Technology, Bachelor's thesis, 2001 |
| Automating Program Verification by Refining Specifications | Mana Taghdiri |
Massachusetts Institute of Technology, PhD thesis, 2008 |
| Lightweight Modeling and Automatic Analysis of Multicast Key Management Schemes | Mana Taghdiri |
Massachusetts Institute of Technology, Master's thesis, 2002 |
| Bounded Verification of an Optimized Shortest Path Implementation |
Michael Nagel |
Karlsruhe Institute of Technology, Studienarbeit, 2012 |
| Proving Alloy models by introducing an explicit relational theory in SMT | Jonathan Best |
Karlsruhe Institute of Technology, Studienarbeit, 2012 |
| Relational Reasoning -- Constraint Solving, Deduction, and Program Verification | Aboubakr Achraf El Ghazi |
Karlsruhe Institute of Technology, PhD thesis, 2015 |
| Generating Bounded Counterexamples for KeY Proof Obligations | Mihai Herda |
Karlsruhe Institute of Technology, Master thesis, 2014 |
| Translating Alloy Specifications to JML |
Daniel Grunwald |
Karlsruhe Institute of Technology, Master thesis, 2013 |
| Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod |
Markus Iser |
Karlsruhe Institute of Technology, Diplomarbeit, 2012 |
| Verifying Alloy Models Using KeY | Ulrich Geilmann |
Karlsruhe Institute of Technology, Diplomarbeit, 2011 |
| Learning-based Software Testing: Evaluation of Angluin's L* Algorithm and Adaptations in Practice | Maximilian X. Czerny |
Karlsruhe Institute of Technology, Bachelor thesis, 2014 |
| Test Case Generation via SSA-based Symbolic Execution | Andreas Fried |
Karlsruhe Institute of Technology, Bachelor Thesis, 2013 |
| Refinement of Path Conditions for Information Flow Analysis | Stephan Gocht |
Karlsruhe Institute of Technology, Bachelor thesis, 2014 |