Publications

Journal Publications

2006–2010

Olga Tveretina, Carsten Sinz, Hans Zantema. Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 7:35-58, 2010.

Olga Tveretina, Carsten Sinz, Hans Zantema. An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas. In Proc. of the 4th Athens Colloquium on Algorithms and Complexity (ACAC 2009), Athens, Greece, August 2009. Published in Electronic Proceedings in Theoretical Computer Science, 4:13-21, 2009. [bib][pdf]

Hendrik Post, Carsten Sinz, Wolfgang Küchlin. Towards Automatic Software Model Checking of Thousands of Linux Modules – A Case Study with Avinux. Software Testing, Verification and Reliability, 19(2):155-172, 2009. [bib][pdf]

Eray Gençay, Carsten Sinz, Wolfgang Küchlin and Thorsten Schäfer. SANchk: SQL-Based SAN Configuration Checking. In IEEE Transactions on Network and Service Management, 5(2):91-104, 2008. [bib][pdf]

Carsten Sinz. Visualizing SAT Instances and Runs of the DPLL Algorithm. J. Automated Reasoning, 39(2):219-243, 2007. [bib][pdf]

Carsten Sinz, Albert Haag, Nina Narodytska, Toby Walsh, Esther Gelle, Mihaela Sabin, Ulrich Junker, Barry O'Sullivan, Rick Rabiser, Deepak Dhungana, Paul Grünbacher, Klaus Lehner, Christian Federspiel, Daniel Naus. Configuration. IEEE Intelligent Systems, 22(1):78-90, 2007. (Report on the ECAI 2006 Workshop on Configuration.) [bib][pdf]

Carsten Sinz, Wolfgang Küchlin, Dieter Feichtinger, and Georg Görtler. Checking Consistency and Completeness of On-Line Product Manuals. J. Automated Reasoning, 37(1-2):45-66, 2006. [bib][pdf]

Armin Biere and Carsten Sinz. Decomposing SAT problems into connected components. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 2:191-198, 2006. [bib][pdf]

2000–2005

Wolfgang Blochinger, Carsten Sinz, and Wolfgang Küchlin. Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Computing, 29(7):969-994, 2003. [bib][pdf]

Carsten Sinz, Andreas Kaiser, and Wolfgang Küchlin. Formal methods for the validation of automotive product configuration data. Artificial Intelligence for Engineering Design, Analysis and Manufacturing, 17(1):75-97, January 2003. Special issue on configuration. [bib][pdf]

Carsten Sinz, Thomas Lumpp, Jürgen Schneider, and Wolfgang Küchlin. Detection of dynamic execution errors in IBM System Automation's rule-based expert system. Information and Software Technology, 44(14):857-873, November 2002. [bib][pdf]

Wolfgang Küchlin and Carsten Sinz. Proving consistency assertions for automotive product data management. J. Automated Reasoning, 24(1-2):145-163, February 2000. [bib][pdf]

Conference Articles

2010

Florian Merz, Carsten Sinz, Hendrik Post, Thomas Gorges, Thomas Kropf. Abstract Testing: Connecting Source Code Verification with Requirements. In Proc. of the 7th Intl. Conf. on Quality of Information and Communications Technology (QUATIC 2010), Oporto, Portugal. To appear.

2009

Hendrik Post, Carsten Sinz, Florian Merz, Thomas Gorges, Thomas Kropf. Linking Functional Requirements and Software Verification. In Proc. of the 17th IEEE Intl. Conf. on Requirements Engineering (RE 2009), pages 295-302, Atlanta, GA, USA. [bib][pdf]

Carsten Sinz, Markus Iser. Problem-Sensitive Restart Heuristics for the DPLL Procedure. In Proc. of the 12th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2009), pages 356-362, Swansea, UK, June 2009. [bib][pdf]

Hendrik Post, Carsten Sinz. Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking. In Proc. of the 2nd Intl. Conf. on Software Testing, Verification and Validation (ICST 2009), pages 31-40, Denver, CO, USA, April 2009. [bib][pdf]

2008

Hendrik Post, Carsten Sinz, Alexander Kaiser, and Thomas Gorges. Reducing False Positives by Combining Abstract Interpretation and Bounded Model Checking. In Proc. of the 23rd IEEE/ACM Intl. Conf. on Automated Software Engineering (ASE 2008), pages 188-197, L'Aquila, Italy, September 2008. [bib][pdf]

Hendrik Post and Carsten Sinz. Configuration Lifting: Software Verification meets Software Configuration. In Proc. of the 23rd IEEE/ACM Intl. Conf. on Automated Software Engineering (ASE 2008), pages 347-350, L'Aquila, Italy, September 2008. [bib][pdf]

Stephan Kottler, Michael Kaufmann, and Carsten Sinz. Computation of Renameable Horn Backdoors. In Proc. of the 11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2008), pages 154-160, Guangzhou, China, May 2008. [bib][pdf]

Stephan Kottler, Michael Kaufmann, and Carsten Sinz. A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors. In Proc. of the 11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2008), pages 161-167, Guangzhou, China, May 2008. [bib][pdf]

Eray Gençay, Carsten Sinz, and Wolfgang Küchlin. Towards SLA-Based Optimal Workload Distribution in SANs. In Proc. of the IFIP/IEEE Network Operations and Management Symposium (NOMS 2008), pages 755-758, Salvador, Brazil, April 2008. [bib][pdf]

2007

Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, and Christoph Wintersteiger. A First Step Towards a Unified Proof Checker for QBF. In Proc. of the 10th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2007), pages 201-214, Lisbon, Portugal, May 2007. [bib][pdf]

Carsten Sinz. Compressing Propositional Proofs by Common Subproof Extraction. In Proc. of the 11th Intl. Conf. on Computer Aided Systems Theory (eurocast 2007), Gran Canaria, Spain, February 2007. [bib][pdf][talk]

2006

Toni Jussila, Carsten Sinz, and Armin Biere. Extended Resolution Proofs for Symbolic SAT Solving with Quantification. In Proc. of the 9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2006), pages 54-60, Seattle, WA, USA, August 2006. [bib][pdf][talk]

Carsten Sinz and Armin Biere. Extended Resolution Proofs for Conjoining BDDs. In Proc. of the 1st Intl. Computer Science Symp. in Russia (CSR 2006), pages 600-611, St. Petersburg, Russia, June 2006. [bib][pdf][talk]

2005

Carsten Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In Proc. of the 11th Intl. Conf. on Principles and Practice of Constraint Programming (CP 2005), pages 827-831, Sitges, Spain, October 2005. [bib][pdf][talk][link]

Carsten Sinz and Edda-Maria Dieringer. DPvis - a tool to visualize structured SAT instances. In Proc. of the 8th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2005), pages 257-268, St. Andrews, UK, June 2005. Springer-Verlag. [bib][pdf][talk][link]

2004

Carsten Sinz and Wolfgang Küchlin. Verifying the on-line help system of SIEMENS magnetic resonance tomographs. In Proc. of the 6th Intl. Conf. on Formal Engineering Methods (ICFEM'2004), pages 391-402, Seattle, WA, November 2004. [bib][pdf][talk]

Murali Sitaraman, Durga P. Gandi, Wolfgang Küchlin, Carsten Sinz, and Bruce B. Weide. DEET for component-based software. In Proceedings of the 2004 SAVCBS Workshop, ACM SIGSOFT 2004/FSE-12, pages 95-104, Newport Beach, CA, USA, October/November 2004. [bib][pdf][talk][link]

Carsten Sinz. Visualizing the internal structure of SAT instances (preliminary report). In Proc. of the 7th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, Canada, May 2004. [bib][pdf][talk][poster][extended]

Carsten Sinz and Wolfgang Küchlin. Verifying the on-line help system of SIEMENS magnetic resonance tomographs using SAT (extended abstract). In Proc. of the 7th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, Canada, May 2004. [bib][pdf][talk][poster]

2003

Carsten Sinz, Amir Khosravizadeh, Wolfgang Küchlin, and Viktor Mihajlovski. Verifying CIM models of Apache web server configurations. In Proc. of the 3rd International Conference on Quality Software (QSIC 2003), pages 290-297, Dallas, TX, November 2003. IEEE Computer Society. [bib][pdf][talk]

Wolfgang Blochinger, Carsten Sinz, and Wolfgang Küchlin. A universal parallel SAT checking kernel. In Hamid R. Arabnia and Youngsong Mun, editors, Proc. of the Intl. Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA'03), volume 4, pages 1720-1725, Las Vegas, NV, June 2003. CSREA Press. [bib][pdf]

2002

Jörg Denzinger, Carsten Sinz, Jürgen Avenhaus, and Wolfgang Küchlin. Teamwork-PaReDuX: Knowledge-based search with multiple parallel agents. In Proceedings of the International Conference on Massively Parallel Computing Systems (MPCS 2002), Ischia, Italy, April 2002. National Technological University Press, Fort Collins, CO. [bib][pdf]

2001

Carsten Sinz, Thomas Lumpp, and Wolfgang Küchlin. Towards a verification of the rule-based expert system of the IBM SA for OS/390 automation manager. In Proceedings of the 2nd Asia-Pacific Conference on Quality Software (APAQS 2001), pages 367-374, Hong Kong, December 2001. IEEE Computer Society. [bib][pdf][talk]

Carsten Sinz, Jörg Denzinger, Jürgen Avenhaus, and Wolfgang Küchlin. Combining parallel and distributed search in automated equational deduction. In Parallel Processing and Applied Mathematics (PPAM 2001), number 2328 in LNCS, Naleczow, Poland, September 2001. Springer-Verlag. [bib][pdf][talk]

Wolfgang Blochinger, Carsten Sinz, and Wolfgang Küchlin. Parallel consistency checking of automotive product data. In Proc. of Intl. Conference Parallel Computing (ParCo 2001), Naples, Italy, September 2001. [bib][pdf]

Wolfgang Blochinger, Carsten Sinz, and Wolfgang Küchlin. Distributed parallel SAT checking with dynamic learning using DOTS. In T. Gonzales, editor, Proc. of the IASTED Intl. Conference Parallel and Distributed Computing and Systems (PDCS 2001), pages 396-401, Anaheim, CA, August 2001. ACTA Press. [bib][pdf]

Carsten Sinz, Andreas Kaiser, and Wolfgang Küchlin. Detection of inconsistencies in complex product model data using extended propositional SAT-checking. In I. Russell and J. Kolen, editors, Proceedings of the 14th International FLAIRS Conference, pages 645-649, Key West, FL, May 2001. AAAI Press. [bib][pdf]

1996–2000

Carsten Sinz. System description: ARA - an automatic theorem prover for relation algebras. In D. McAllester, editor, Automated Deduction (CADE-17), number 1831 in LNAI, pages 177-182, Pittsburgh, PA, June 2000. Springer-Verlag. [bib][pdf][talk][leaflet]

Ralf-Dieter Schimkat, Wolfgang Blochinger, Carsten Sinz, Michael Friedrich, and Wolfgang Küchlin. A service-based agent framework for distributed symbolic computation. In M. Bubak, R. Williams, H. Afsarmanesh, and B. Hertzberger, editors, Proc. 8th Intl. Conf. on High Performance Computing and Networking Europe (HPCN 2000), number 1823 in LNCS, pages 644-656, Amsterdam, Netherlands, May 2000. Springer-Verlag. [bib][pdf]

Reinhard Bündgen, Carsten Sinz, and Jochen Walter. ReDuX 1.5: New facets of rewriting. In Harald Ganzinger, editor, Rewriting Techniques and Application (RTA-96), number 1103 in LNCS, pages 412-415, New Brunswick, NJ, July 1996. Springer-Verlag. [bib][link]

Reviewed Workshop Papers

2006–2010

Carsten Sinz, Stephan Falke, Florian Merz. A Precise Memory Model for Low-Level Bounded Model Checking. In Proc. of the 5th Intl. Workshop on Systems Software Verification (SSV 2010), Vancouver, Canada, October 2010. To appear.

Mana Taghdiri, Gregor Snelting, Carsten Sinz. Information Flow Analysis via Path Condition Refinement. In Proc. of the 7th Intl. Workshop on Formal Aspects of Security & Trust (FAST 2010), Pisa, Italy, September 2010. To appear.

Eray Gençay, Carsten Sinz, and Wolfgang Küchlin. SLA-Based SAN Design. In Proc. of the 1st IEEE Workshop on Automated Network Management (ANM 2008), Phoenix, AZ, April 2008. [bib][pdf]

Hendrik Post, Carsten Sinz, and Wolfgang Küchlin. Avinux: Towards Automatic Verification of Linux Device Drivers. In ProVeCS Workshop Proceedings, TOOLS Europe 2007: Object, Models, Components and Patterns, Zurich, Switzerland, June 2007. [bib][pdf][talk][link]

Carsten Sinz. Comparing Different Logic-Based Representations of Automotive Parts Lists. In Configuration Workshop Proceedings, 17th European Conference on Artificial Intelligence (ECAI-2006), Riva del Garda, Italy, August 2006. [bib][pdf][talk]

2000–2005

Carsten Sinz and Wolfgang Küchlin. Co-configuration of products and on-line service manuals. In Configuration Workshop Proceedings, 19th International Joint Conference on Artificial Intelligence (IJCAI-05), Edinburgh, UK, July 2005. [bib][pdf][talk]

Carsten Sinz. Knowledge compilation for product configuration. In Configuration Workshop Proceedings, 15th European Conference on Artificial Intelligence (ECAI-2002), pages 23-26, Lyon, France, July 2002. [bib][pdf][talk]

Carsten Sinz. Formal verification in an industrial context. In Symposium on the Effectiveness of Logic in Computer Science (ELICS'02), pages 59-63, Saarbrücken, Germany, March 2002. In Technical Report MPI-I-2002-2-007. [bib][pdf][talk]

Carsten Sinz and Wolfgang Küchlin. Dealing with temporal change in product documentation for manufacturing. In Configuration Workshop Proceedings, 17th International Joint Conference on Artificial Intelligence (IJCAI-2001), pages 71-77, Seattle, WA, August 2001. [bib][pdf][talk]

Carsten Sinz, Wolfgang Blochinger, and Wolfgang Küchlin. PaSAT - parallel SAT-checking with lemma exchange: Implementation and applications. In H. Kautz and B. Selman, editors, LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001), volume 9 of Electronic Notes in Discrete Mathematics, Boston, MA, June 2001. Elsevier Science Publishers. [bib][pdf][talk]

Carsten Sinz, Andreas Kaiser, and Wolfgang Küchlin. SAT-based consistency checking of automotive electronic product data. In Configuration Workshop Proceedings, 14th European Conference on Artificial Intelligence (ECAI-2000), pages 74-78, Berlin, Germany, August 2000. [bib][pdf][talk]

Theses

Carsten Sinz. Verifikation regelbasierter Konfigurationssysteme. PhD thesis (Dissertation, in German), December 2003. [bib][pdf][talk][errata][link]

Carsten Sinz. Baubarkeitsprüfung von Kraftfahrzeugen durch automatisches Beweisen. Master thesis (Diplomarbeit, in German), December 1997. [bib][pdf]

Carsten Sinz. Untersuchung und Implementation der Reduktionskalküle RPC_n. Semester project (Studienarbeit, in German), June 1997. [bib][pdf]

Technical Reports

Carsten Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints (Technical Report). October 2005. [pdf][link]

Miscellaneous

Carsten Sinz. Software Verification: State of the Art and Challenges. In V. Pankratius, S. Kounev, editors, Emerging Research Directions in Computer Science – Contributions from the Young Informatics Faculty in Karlsruhe, pages 69-77. KIT Scientific Publishing, Karlsruhe, Germany, 2010.

Murali Sitaraman, Durga P. Gandi, Wolfgang Küchlin, Carsten Sinz, and Bruce B. Weide. The humane bugfinder: Modular static analysis using a SAT solver. Technical Report RSRG-03-05, Department of Computer Science, Clemson University, SC, June 2003. [bib][pdf][link]

Andrea Sinz and Carsten Sinz. Software development for determining cross-linking sites in proteins. Poster, 35. Diskussionstagung der Deutschen Gesellschaft für Massenspektrometrie (DGMS 2002), Heidelberg, Germany, March 2002. [bib][poster]

Wolfgang Küchlin and Carsten Sinz. Proving consistency assertions for automotive product data management. In I. Gent, H. van Maaren, and T. Walsh, editors, SAT2000 - Highlights of Satisfiability Research in the Year 2000, volume 63 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2000. [bib][pdf]