Research Assistant at Chair of Computer Architecture. Research interests: SAT, BDDs, Verification. [Contact]     [Publications and Talks]     [Supervised Courses]     [Supervised Students]     [Research Projects] [Miscellaneous]

Contact [top]

This address is obsolete. Please contact me via marc.herbstritt(at)acm.org or visit my webpage at Schloss Dagstuhl--Leibniz-Center for Informatics
• Marc Herbstritt
  Fakultät für angewandte Wissenschaften
  Albert-Ludwigs-Universität
  Georges-Köhler-Allee, Geb. 51, Raum 01-033
  79110 Freiburg im Breisgau
  Deutschland
  
  Telefon: ++49 +761 203-8147
  Fax: ++49 +761 203-8142
  eMail: herbstri(at)informatik.uni-freiburg.de

Publications and Talks [top]     [check DBLP]   [ACM profile]

• Böde, Eckard and Herbstritt, Marc and Hermanns, Holger and Johr, Sven and Peikenkamp, Thomas and Pulungan, Reza and Rakow, Jan and Wimmer, Ralf and Becker, Bernd
  Compositional Dependability Evaluation for STATEMATE
  In IEEE Transactions on Software Engineering, Special Issue on Quantitive Evaluation of Computer Systems (Guest Editors: Jane Hillston, Marta Kwiatkowska, Miklos Telek), Vol.35, No.2, March/April 2009, pp.274-292.
    [BiBTeX]  

• Marc Herbstritt Satisfiability & Verification: From Core Algorithms to Novel Application Domains 236 p., February 2009. SVH Verlag. ISBN 978-3-8381-0102-6.       [BiBTeX]

• Becker, Bernd and Herbstritt, Marc and Kalinnik, Natalia and Lewis, Matthew and Lichtner, Juri and Nopper, Tobias and Wimmer, Ralf
  Propositional Approximations for Bounded Model Checking of Partial Circuit Designs
  In Proceedings of IEEE International Conference on Computer Design (ICCD), Resort at Squaw Creek, Lake Tahoe, CA, USA, October 12-15 2008. IEEE Computer Society. ISBN 978-1-4244-2657-7.
    [slides (pdf)]   [BiBTeX]  
• Wimmer, Ralf and Kortus, Alexander and Herbstritt, Marc and Becker, Bernd
  Probabilistic Model Checking and Realibility of Results
  In Proceedings of 11th IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems (DDECS), Bratislava, Slovakia, April 16.-18. 2008. IEEE Computer Society.
    [slides (pdf)]   [BiBTeX]  
• Wimmer, Ralf and Kortus, Alexander and Herbstritt, Marc and Becker, Bernd
  The Demand for Reliability in Probabilistic Verification
  In Proceedings of 11th ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Freiburg, Germany, pp. 99-108, March 03-05 2008. ISBN 978-3-8322-6962-3.
  [Shaker]   [slides (pdf)]   [BiBTeX]
• Marc Herbstritt
  SAT-based Verification - From Core Algorithms to Novel Application Domains
  Dissertation, Albert-Ludwigs-Universität Freiburg im Breisgau, 29. Februar 2008.
• Herbstritt, Marc and Struve, Vanessa and Becker, Bernd
  Application of Lifting in Partial Design Analysis
  In Proceedings of 8th IEEE International Workshop on Microprocessor Test and Verification (MTV 2007), Austin (TX), USA, December 04-06 2007. IEEE Computer Society.
    [slides (pdf)] [BiBTeX]
• Wimmer, Ralf and Kortus, Alexander and Herbstritt, Marc and Becker, Bernd
  Symbolic Model Checking of DTMCs with Exact and Inexact Arithmetic
  AVACS Technical Report, No. 30, SFB/TR 14 AVACS, August 2007. ISSN: 1860-9821, www.avacs.org.
    [BiBTeX]  
• Wimmer, Ralf and Hermanns, Holger and Herbstritt, Marc and Becker, Bernd
  Towards Symbolic Stochastic Aggregation
  AVACS Technical Report, No. 16, SFB/TR 14 AVACS, August 2007. ISSN: 1860-9821, www.avacs.org.
    [BiBTeX]  
• Herbstritt, Marc and Becker, Bernd and Ábrahám, Erika and Herde, Christian
  On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata
  In Proceedings of 10th IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems (DDECS), Kraków, Poland, April 11-13 2007. IEEE Computer Society. ISBN 1-4244-1161-0.
    [slides (pdf)]   [BiBTeX]
• Wimmer, Ralf and Herbstritt, Marc and Becker, Bernd
  Optimization Techniques for BDD-based Bisimulation Computation
  In Proceedings of 17th ACM Great Lakes Symposium on VLSI (GLSVLSI), pp. 405--410, Stresa-Lago Maggiore, Italy, March 11-13 2007. ISBN 978-1-59593-605-9.
    [slides (pdf)]   [BiBTeX]
• Wimmer, Ralf and Herbstritt, Marc and Becker, Bernd
  Forwarding, Splitting, and Block Ordering to Optimize BDD-based Bisimulation Computation
  In Proceedings of 10th ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), pp. 203-212, Erlangen, Germany, March 05-07 2007. ISBN 978-3-8322-5956-3.
  [pdf]   [slides (pdf)]   [BiBTeX]
• Herbstritt, Marc and Becker, Bernd
  On Combining 01X-Logic and QBF
  In Proceedings of 11th International Conference on Computer Aided Systems Theory, Applied Formal Verification Track, (EuroCAST 2007), Revised Selected Papers, pp. 531-538, Las Palmas de Gran Canaria, Canary Islands, Spain, February 12-16 2007. Springer LNCS 4739. ISBN 978-3540758662.
    [slides (pdf)]   [BiBTeX]  
• Herbstritt, Marc and Becker, Bernd and Scholl, Christoph
  Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs
  In Proceedings of 7th IEEE International Workshop on Microprocessor Test and Verification (MTV 2006), pp. 37-44, Austin (TX), USA, December 04-05 2006. IEEE Computer Society. ISBN-10 0-7695-2839-2.
    [slides (pdf)]   [BiBTeX]
• Wimmer, Ralf and Herbstritt, Marc and Hermanns, Holger and Strampp, Kelley and Becker, Bernd
  Sigref - A Symbolic Bisimulation Tool Box
  In Proceedings of 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), Beijing, China, October 23.-26. 2006. Springer LNCS 4218. ISBN 978-3-540-47237-7.
    [slides (pdf)]   [BiBTeX]
• Wimmer, Ralf and Nopper, Tobias and Herbstritt, Marc and Löffler, Christoph and Becker, Bernd
  Collaborative Exercise Management
  In Proceedings of World Conference on E-Learning in Corporate, Government, Healthcare, & Higher Education (E-Learn), pp. 3127--3134, Honolulu, Hawaii, USA, October 13.-17. 2006. ISBN 1-8800-9460-6.
    [slides (pdf)]   [BiBTeX]
• Böde, Eckard and Herbstritt, Marc and Hermanns, Holger and Johr, Sven and Peikenkamp, Thomas and Pulungan, Reza and Wimmer, Ralf and Becker, Bernd
  Compositional Performability Evaluation for STATEMATE
  In Proceedings of 3rd International Conference on the Quantitative Evaluation of SysTems (QEST), Riverside (CA), USA, September 11.-14. 2006. IEEE Computer Society. ISBN 0-7695-2665-9.
    [BiBTeX]  
• Ábrahám, Erika and Herbstritt, Marc and Becker, Bernd and Steffen, Martin
  Bounded Model Checking with Parametric Data Structures
  In Proceedings of 4th International Workshop on Bounded Model Checking (BMC), pp. 3--16, Electronic Notes in Theoretical Computer Science (ENTCS), vol. 174, issue 3, Elsevier. Seattle, USA, August 15 2006.
    [slides (pdf)]   [BiBTeX]
• Wimmer, Ralf and Herbstritt, Marc and Becker, Bernd
  Minimization of Large State Spaces using Symbolic Branching Bisimulation
  In Proceedings of 9th IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems (DDECS), Praha, Czech Republic, April 18.-21. 2006. IEEE Computer Society. ISBN 1-4244-0184-4.
    [slides (pdf)]   [BiBTeX]  
• Herbstritt, Marc and Wimmer, Ralf and Peikenkamp, Thomas and Böde, Eckard and Adelaide, Michael and Johr, Sven and Hermanns, Holger and Becker, Bernd
  Analysis of Large Safety-Critical Systems: A quantitative Approach
  AVACS Technical Report, No. 8, SFB/TR 14 AVACS, February 2006. ISSN: 1860-9821, www.avacs.org.
    [BiBTeX]  
• Ábrahám, Erika and Herbstritt, Marc and Becker, Bernd and Steffen, Martin
  Memory-aware Bounded Model Checking for Linear Hybrid Systems
  In Proceedings of 9th ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), pp. 153-162, Dresden, Germany, February 2006. ISBN 3-9810287-1-6.
  [ps.gz]   [pdf]   [slides (pdf)]   [BiBTeX]  
• Herbstritt, Marc and Becker, Bernd
  On SAT-based Bounded Invariant Checking of Blackbox Designs
  In Proceedings of 6th IEEE International Workshop on Microprocessor Test and Verification (MTV 2005), pp. 23-28, Austin (TX), USA, November 03-04 2005. IEEE Computer Society. ISBN-13 0-7695-2627-0.
    [slides (pdf)]   [BiBTeX]
• Herbstritt, Marc and Kmieciak, Thomas and Becker, Bernd
  On the Impact of Structural Circuit Partitioning on SAT-based Combinational Circuit Verification
  In Proceedings of 5th IEEE International Workshop on Microprocessor Test and Verification (MTV 2004), pp. 50-55, ISBN-0-7695-2320-X, Austin (TX), USA, September 08-10 2004. IEEE Computer Society. ISBN 0-7695-2320-X.
    [slides (pdf)]   [printable slides (pdf)]   [BiBTeX]
• Herbstritt, Marc and Kmieciak, Thomas and Becker, Bernd
  Circuit Partitioning for SAT-based Combinational Circuit Verification - A Case Study
  Technical Report 206, Albert-Ludwigs-University, Freiburg, July 2004.
  [ps.gz]   [pdf]   [BiBTeX]
• Becker, Bernd and Behle, Markus and Eisenbrand, Fritz and Fränzle, Martin and Herbstritt, Marc and Herde, Christian and Hoffmann, Jörg and Kröning, Daniel and Nebel, Bernhard and Polian, Ilia and Wimmer, Ralf
  Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems
  In Proceedings of 7th GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pp. 65-75, Kaiserslautern, Germany, February 2004. ISBN 3-8322-2486-6.
  [pdf]   [BiBTeX]  
• Herbstritt, Marc and Becker, Bernd
  Conflict-based Selection of Branching Rules
  In Enrico Giunchiglia and Armando Tacchella, editors, Proceedings of 6th International Conference on Theory and Applications in Satisfiability Testing (SAT2003), pp. 441-451. Santa Margherita Ligure - Portofino, Italy, May 5-8 2003. Selected Revised Papers. Springer LNCS 2919. ISBN 978-3-540-20851-8.
    [preprint pdf]   [slides (pdf)]   [slides (HTML)]   [BiBTeX]  
• Herbstritt, Marc and Becker, Bernd
  Conflict-based Selection of Branching Rules in SAT-Algorithms
  In Proceedings of 6th GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Bremen, Germany, pp. 189-198, February 2003.
  [ps.gz]   [pdf]   [slides (pdf)]   [slides (HTML)]   [BiBTeX]  
• Herbstritt, Marc
  zChaff: Modifications and Extensions
  Technical Report 188, Albert-Ludwigs-University, Freiburg, July 2003.
  [ps.gz]   [pdf]  
• Scholl, Christoph and Herbstritt, Marc and Becker, Bernd
  Exploiting Don't Cares to Minimize *BMDs
  In Proceedings IEEE International Symposium on Circuits and Systems, Sidney, Australia, May 06-09 2001. IEEE Computer Society. ISBN 0-7803-6685-9.
    [PowerPoint]   [HTML]   [BiBTeX]
• Scholl, Christoph and Herbstritt, Marc and Becker, Bernd
  Don't Care Minimization of *BMDs: Complexity and Algorithms
  In Proceedings of 4th GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Meißen, Germany, pp. 45-57, February 2001.
  [ps.gz]   [pdf]   [PowerPoint]   [HTML]   [BiBTeX]  
• Scholl, Christoph and Herbstritt, Marc and Becker, Bernd
  Exploiting Don't Cares to Minimize *BMDs
  Technical Report 141, Albert-Ludwigs-University, Freiburg, September 2000.
  [ps.gz]   [pdf]   [BiBTeX]
• Herbstritt, Marc
  Erfüllbarkeitsprobleme bei Word-Level Decision Diagrams
  Diplomarbeit, April 2000.
  [ps.gz]   [pdf]   [BibTex]
• Drechsler, Rolf and Herbstritt, Marc and Becker, Bernd
  Grouping Heuristics for Word-level Decision Diagrams
  In Proceedings of IEEE International Symposium on Circuits and Systems, Orlando, Florida, USA, pp. 411-414, 30 May-02 June 1999. IEEE Computer Society. ISBN 0-7803-5471-0.
    [PowerPoint]   [BiBTeX]
• Drechsler, Rolf and Herbstritt, Marc and Becker, Bernd
  Grouping Heuristics for Word-level Decision Diagrams
  In Proceedings of 2nd GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Braunschweig, Germany, pp. 41-50, February 1999.
  [ps.gz]   [pdf]   [PowerPoint]   [HTML]   [BiBTeX]
• Herbstritt, Marc
  Implementation eines *BMD-Pakets
  Studienarbeit, October 1997.
  [ps.gz]   [pdf]

Supervised Courses [top]

[KV=Kursvorlesung, SV=Spezialvorlesung, S=Seminar]

• Systeme I (KV) im Wintersemester 2006/07.
• Advanced Model Checking (S) im Wintersemester 2005/06.
• Technische Informatik (KV) im Wintersemester 2004/05.
• AVACS: Analysis and Verification of Complex Systems (S) im Sommersemester 2003.
• Formale Verifikation von Hardware (SV) im Wintersemester 2002/03.
• Technische Informatik I (KV) im Wintersemester 2001/02.
• Technische Informatik I (KV) im Wintersemester 2000/01.

Supervised Students [top]