Home  |  Legals  |  Data Protection  |  Sitemap  |  KIT

Mihai Herda

Mihai Herda 2014 M.Sc. Mihai Herda - Researcher / PhD Student
Am Fasanengarten 5
Building 50.34
Office 227
76131 Karlsruhe
Germany

Tel.: + 49 721 608 43856
Fax: + 49 721 608 44021
Email: herda∂kit edu


Projects


Teaching

  • Praxis der Softwareentwicklung: WS 14/15, WS 17/18, SS 18
  • (Pro)seminar: WS 14/15, SS 15, WS 15/16, SS 16, SS 17, WS 18/19, SS 19
  • Praxis der Forschung: WS 15/16 , SS 16, WS 16/17, SS 17
  • Formale Systeme: WS 16/17, WS 17/18, WS 18/19, WS 19/20

  • Publications

    2019
    Title Author(s) Source
    Using Relational Verification for Program SlicingBernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich17th International Conference on Software Engineering and Formal Methods (SEFM 2019)
    Understanding Counterexamples for Relational Properties with DIbuggerMihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick, and Bernhard BeckertSixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning (HCVS/PERR 2019)
    Using Relational Verification for Program SlicingBernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias UlbrichDepartment of Informatics, Karlsruhe Institute of Technology 2019,5
    Verification-based Test Case Generation for Information-Flow PropertiesMihai Herda, Shmuel Tyszberowicz, Joachim Müssig, and Bernhard Beckert34rd Annual ACM Symposium on Applied Computing (SAC 2019)
    2018
    Title Author(s) Source
    Formal Specification and Verification of Hyperledger Fabric ChaincodeBernhard Beckert, Mihai Herda, Michael Kirsten, and Jonas Schiffl3rd Symposium on Distributed Ledger Technology (SDLT-2018) co-located with ICFEM 2018: the 20th International Conference on Formal Engineering Methods
    A Uniform Information-Flow-Security Benchmark Suite for Source Code and BytecodeTobias Hamann, Mihai Herda, Heiko Mantel, Martin Mohr, David Schneider, and Markus Tasch23rd Nordic Conference on Secure IT Systems (NordSec 2018)
    Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow ControlBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning20th International Conference on Formal Engineering Methods - Formal Methods and Software Engineering (ICFEM 2018)
    Towards a Notion of Coverage for Incomplete Program-Correctness ProofsBernhard Beckert, Mihai Herda, Stefan Kobischke, and Mattias Ulbrich8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018), Part II: A Broader View on Verification: From Static to Runtime and Back
    Using Dependence Graphs to Assist Verification and Testing of Information-Flow PropertiesMihai Herda, Shmuel Tyszberowicz, and Bernhard Beckert12th International Conference on Tests and Proofs (TAP 2018)
    2017
    Title Author(s) Source
    SemSlice: Exploiting Relational Verification for Automatic Program SlicingBernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich13th International Conference on integrated Formal Methods (iFM 2017)
    RIFL 1.1: A Common Specification Language for Information-Flow RequirementsThomas Bauereiß, Simon Greiner, Mihai Herda, Michael Kirsten, Ximeng Li, Heiko Mantel, Martin Mohr, Matthias Perner, David Schneider, and Markus TaschTU Darmstadt TUD-CS-2017-0225
    Combining Graph-Based and Deduction-Based Information-Flow AnalysisBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017) affiliated with ETAPS 2017: European Joint Conferences on Theory and Practice of Software
    CoCoME with SecuritySimon Greiner and Mihai HerdaDepartment of Informatics, Karlsruhe Institute of Technology 2017,2
    2016
    Title Author(s) Source
    Proof-based Test Case GenerationWolfgang Ahrendt, Christoph Gladisch, and Mihai HerdaDeductive Software Verification - The KeY Book: From Theory to Practice, Part III: From Verification to Analysis
    Computing Specification-Sensitive Abstractions for Program VerificationTianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl, and Mana TaghdiriSecond International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016)
    Security in E-VotingDaniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel, and Richard GayPoster at the 25th USENIX Security Symposium
    2015
    Title Author(s) Source
    Poster: Security in E-VotingDaniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel, and Richard Gay36th IEEE Symposium on Security and Privacy (S&P 2015), Poster Session
    First-Order Transitive Closure Axiomatization via Iterative Invariant InjectionsAboubakr Achraf El Ghazi, Mana Taghdiri, and Mihai Herda7th NASA Formal Methods Symposium (NFM 2015)
    2014
    Title Author(s) Source
    The KeY Platform for Verification and Analysis of Java ProgramsWolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014)
    Generating Bounded Counterexamples for KeY Proof ObligationsMihai HerdaKarlsruhe Institute of Technology (January 2014)
    2013
    Title Author(s) Source
    Reducing the Complexity of Quantified Formulas via Variable EliminationAboubakr Achraf El Ghazi, Mattias Ulbrich, Mana Taghdiri, and Mihai Herda11th International Workshop on Satisfiability Modulo Theories (SMT 2013)


    Data & Software

    2019
    Title Author(s) Source
    Implementation of the Combined ApproachBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, Marko Kleine Büning, Holger Klein, and Joachim Müssighttps://doi.org/10.5281/zenodo.3359433
    Evaluation Data of the Combined ApproachBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, Holger Klein, Marko Kleine Büning, and Joachim Müssighttps://doi.org/10.5281/zenodo.3359387
    Implementation of DIbuggerMihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick, and Bernhard Beckerthttps://doi.org/10.5281/zenodo.3334650
    Evaluation Data of the Implementation of the Approach for Automatic Test Generation for Information-Flow PropertiesMihai Herda, Shmuel Tyszberowicz, Joachim Müssig, and Bernhard Beckerthttps://doi.org/10.5281/zenodo.3334380
    Implementation of the Approach for Automatic Test Generation for Information-Flow PropertiesMihai Herda, Shmuel Tyszberowicz, Joachim Müssig, and Bernhard Beckerthttps://doi.org/10.5281/zenodo.3334532
    Implementation of the SemSlice ToolBernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrichhttps://doi.org/10.5281/zenodo.3334553
    Evaluation Data of SemSliceBernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrichhttps://doi.org/10.5281/zenodo.3334571