Florian Pigorsch
Contact
Dipl.-Inf. Florian Pigorsch
Albert-Ludwigs-Universität FreiburgInstitut für Informatik
Lehrstuhl für Betriebssysteme
Georges-Koehler-Allee 51
D-79110 Freiburg
Room 51-02-032
Tel: +49-761-203-8196
Fax: +49-761-203-8142
Email: pigorsch@informatik.uni-freiburg.de
S/MIME Certificate: Florian_Pigorsch.pem, valid until 2013-11-25, Trust Chain: Deutsche Telekom, DFN, Uni-Fr
Research & Projects
- And-Inverter Graphs (AIG), an efficient data-structure for representing and manipulating Boolean functions
- Quantified Boolean Formulae (QBF) solving using And-Inverter Graphs as means of symbolic representation (AIGSolve)
- Symbolic CTL-Model Checking
- Transregional Collaborative Research Center 14: Automatic Verification and Analysis of Complex Systems (AVACS): Main AVACS site, GForge server
Publications
2011
-
Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
Werner Damm,
Henning Dierks,
Stefan Disch,
Willem Hagemann,
Florian Pigorsch,
Christoph Scholl,
Uwe Waldmann, and
Boris Wirtz
In "Science of Computer Programming", Special Issue on Automated Verification of Critical Systems, 2011
Elsevier -
Fully Symbolic Model Checking for Timed Automata
Georges Morbé,
Christoph Scholl, and
Florian Pigorsch
In Proceedings of "Computer Aided Verification" (CAV11), 2011, Snowbird, Utah
Springer, Timed Systems Benchmarks -
Integration of Orthogonal QBF Solving Techniques
Sven Reimer,
Florian Pigorsch,
Christoph Scholl, and
Bernd Becker
In Proceedings of "Design, Automation and Test in Europe" (DATE11), March 2011, Grenoble, France
IEEE Xplore
2010
-
An AIG-Based QBF-solver using SAT for preprocessing
Florian Pigorsch,
Christoph Scholl
In Proceedings of the 47th "Design Automation Conference" (DAC47), pages 170-175, June 2010, Anaheim, CA, USA
pigorsch-dac10.pdf, IEEE Xplore
2009
-
Exploiting Structure in an AIG Based QBF Solver
Florian Pigorsch,
Christoph Scholl
Proc. Conf. on "Design, Automation and Test in Europe" (DATE09), April 2009, Nice, France
pigorsch-date09.pdf -
Using Implications for Optimizing State Set Representations of Linear Hybrid Systems
Florian Pigorsch,
Christoph Scholl
11th ITG/GI/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", March 2009, Berlin, Germany
pigorsch-mbmv09.pdf -
Computing optimized representations for non-convex polyhedra by detection and removal of redundant linear constraints
Christoph Scholl,
Stefan Disch,
Florian Pigorsch,
Stefan Kupferschmid
Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2009, York, UK
SDPK_2009.pdf
2008
-
Using an SMT Solver and Craig Interpolation to Detect and Remove Redundant Linear Constraints in Representations of Non-Convex Polyhedra
Christoph Scholl,
Stefan Disch,
Florian Pigorsch,
Stefan Kupferschmidt
International Workshop on "Satisfiability Modulo Theories", July 2008, Princeton, USA
bibtex
2007
-
Exact state set representation in the verification of linear hybrid systems with large discrete state space
Werner Damm,
Stefan Disch,
Hardi Hungar,
Swen Jacobs,
Jun Pang,
Florian Pigorsch,
Christoph Scholl,
Uwe Waldmann,
and Boris Wirtz
To appear in 5th International Symposium on Automated Technology for Verification and Analysis, Tokyo, Japan, October 22-25, 2007.
ddhp+2007.pdf, bibtex
2006
-
Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling
Florian Pigorsch, Christoph Scholl, and Stefan Disch
In Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD 2006), pages 89-96, November 12-16 2006, San Jose, CA, USA. IEEE Computer Society Press.
psd2006b.pdf, psd2006b.bib, IEEE Xplore -
Automatic Verification of Hybrid Systems with Large Discrete State Space
Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz
In Susanne Graf and Wenhui Zhang, editors, Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, LNCS 4218, pages 276-291, Beijing, China, October 23-26, 2006. Springer-Verlag.
ddhp+2006.pdf, ddhp+2006.bib, SpringerLink -
Advanced unbounded model checking by using AIGs, BDD sweeping and quantifier scheduling
Florian Pigorsch, Christoph Scholl, and Stefan Disch
9th ITG/GI/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", February 2006, Dresden, Germany
psd2006.pdf, psd2006.bib
2005
-
And-Inverter-Graphen und deren Anwendung in der Verifikation
Florian Pigorsch
Diplomarbeit, Albert-Ludwigs-Universität Freiburg, July 2005
Events
2008
- 11. Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen": organizational support
2007
- 12th IEEE European Test Symposium, ETS07: organizational support
Teaching Support
Winter Term 2011
- Organisation and assistance for the lecture Syteme 1
Summer Term 2010
- Organisation and assistance for the lab Modellierung eingebetteter Systeme
Winter Term 2009/2010
- Partial lecturing of Eingebettete Systeme I
Summer Term 2009
Winter Term 2008/2009
- Organisation and assistance for the lecture Verifikation eingebetteter Systeme
Summer Term 2008
- Organisation and assistance for the lab Entwurf eingebetteter Systeme mit Statecharts and the student project Modellierung eingebetteter Systeme
Winter Term 2006/2007
- Organisation and assistance for the lecture Technische Informatik
Summer Term 2006
- Assistance for the seminar Verifikation und Fehlerdiagnose
Various Interesting Things
- My Erdős-Number is (at most) 4: (Paul Erdős - Frank Harary - John P. Hayes - Bernd Becker - me) or (Paul Erdős - Saharon Shelah - Amir Pnueli - Werner Damm - me) or ...