Carsten Sinz's bibTeX file



@INPROCEEDINGS{JussilaSinzBiere:06,
	Author = {Toni Jussila and Carsten Sinz and Armin Biere},
	Title = {Extended Resolution Proofs for Symbolic SAT Solving
	         with Quantification},
	Booktitle = {Proc.\ of the 9th Intl.\ Conf.\ on Theory and Applications
		of Satisfiability Testing ({SAT 2006})},	
	Month = aug,
	Year = 2006,
    Address = {Seattle, WA},
    Publisher = {Springer-Verlag},
	Pages = {54--60}
}


@INPROCEEDINGS{Sinz:06,
	Author = {Carsten Sinz},
	Title = {Comparing Different Logic-Based Representations of
	         Automotive Parts Lists},
	Booktitle = {Configuration Workshop Proceedings, 17th European
		         Conference on Artificial Intelligence ({ECAI 2006})},
	Year = 2006,
	Month = aug,
	Address = {Riva del Garda, Italy}
}


@INPROCEEDINGS{SinzBiere:06,
  AUTHOR = {Carsten Sinz and Armin Biere},
  TITLE = {Extended Resolution Proofs for Conjoining {BDDs}},
  BOOKTITLE = {Proc.\ of the 1st Intl.\ Computer Science Symp.\ in Russia
    ({CSR 2006})},
  YEAR = 2006,
  MONTH = jun,
  ADDRESS = {St. Petersburg, Russia},
  PAGES = {600--611}
}


@ARTICLE{BiereSinz:06,
  AUTHOR = {Armin Biere and Carsten Sinz},
  TITLE = {Decomposing {SAT} Problems into Connected Components},
  JOURNAL = {Journal on Satisfiability, Boolean Modeling and Computation},
  PUBLISHER = {Delft University},
  ISSN = {1574-0617},
  VOLUME = 2,
  PAGES = {191--198},
  YEAR = 2006
}


@INPROCEEDINGS{Sinz:05,
  AUTHOR = {Carsten Sinz},
  TITLE = {Towards an Optimal {CNF} Encoding of Boolean Cardinality
		Constraints},
  BOOKTITLE = {Proc.\ of the 11th Intl.\ Conf.\ on Principles and Practice
		of Constraint Programming ({CP 2005})},
  YEAR = 2005,
  MONTH = OCT,
  ADDRESS = {Sitges, Spain},
  PAGES = {827--831}
}


@INPROCEEDINGS{SinzKuechlin:05,
  AUTHOR = {Carsten Sinz and Wolfgang K{\"u}chlin},
  TITLE = {Co-Configuration of Products and On-Line Service Manuals},
  BOOKTITLE = {Configuration Workshop Proceedings, 19th International
		Joint Conference on Artificial Intelligence ({IJCAI-05})},
  YEAR = 2005,
  MONTH = JUL,
  ADDRESS = {Edinburgh, Scotland}
}


@INPROCEEDINGS{SinzDieringer:05,
  AUTHOR = {Carsten Sinz and Edda-Maria Dieringer},
  TITLE = {{DPvis} - A Tool to Visualize Structured {SAT} Instances},
  BOOKTITLE = {Proc.\ of the 8th Intl.\ Conf.\ on Theory and Applications
		of Satisfiability Testing ({SAT 2004})},
  MONTH = JUN,
  YEAR = 2005,
  ADDRESS = {St. Andrews, Scotland},
  PUBLISHER = {Springer-Verlag},
  PAGES = {257--268}
}


@INPROCEEDINGS{SinzKuechlin:04b,
  AUTHOR = {Carsten Sinz and Wolfgang K{\"u}chlin},
  TITLE = {Verifying the On-Line Help System of {SIEMENS} Magnetic
		Resonance Tomographs},
  BOOKTITLE = {Proc.\ of the 6th Intl.\ Conf.\ on Formal Engineering
		Methods (ICFEM'2004)},
  MONTH = NOV,
  YEAR = 2004,
  ADDRESS = {Seattle, WA},
  PAGES = {391--402}
}


@INPROCEEDINGS{Sitaraman-etal:04,
  AUTHOR = {Murali Sitaraman and Durga P. Gandi and Wolfgang K{\"u}chlin
 		and Carsten Sinz and Bruce B. Weide},
  TITLE = {{DEET} for Component-Based Software},
  BOOKTITLE = {Proceedings of the 2004 SAVCBS Workshop, 
              ACM SIGSOFT 2004/FSE-12},
  MONTH = OCT,
  YEAR = 2004,
  ADDRESS = {Newport Beach, CA},
  PAGES = {95--104}
}


@INPROCEEDINGS{Sinz:04,
  AUTHOR = {Carsten Sinz},
  TITLE = {Visualizing the Internal Structure of {SAT} Instances
		(Preliminary Report)},
  BOOKTITLE = {Proc.\ of the 7th Intl.\ Conf.\ on Theory and Applications
		of Satisfiability Testing ({SAT 2004})},
  MONTH = MAY,
  YEAR = 2004,
  ADDRESS = {Vancouver, Canada}
}


@INPROCEEDINGS{SinzKuechlin:04a,
  AUTHOR = {Carsten Sinz and Wolfgang K{\"u}chlin},
  TITLE = {Verifying the On-Line Help System of {SIEMENS} Magnetic
		Resonance Tomographs using {SAT} (Extended Abstract)},
  BOOKTITLE = {Proc.\ of the 7th Intl.\ Conf.\ on Theory and Applications
		of Satisfiability Testing ({SAT 2004})},
  MONTH = MAY,
  YEAR = 2004,
  ADDRESS = {Vancouver, Canada}
}


@INPROCEEDINGS{Sinz-etal:03,
  AUTHOR = {Carsten Sinz and Amir Khosravizadeh and Wolfgang K{\"u}chlin
		and Viktor Mihajlovski},
  TITLE = {Verifying {CIM} Models of {Apache} Web Server Configurations},
  BOOKTITLE = {Proc.\ of the 3rd International Conference on
		Quality Software ({QSIC 2003})},
  YEAR = 2003,
  MONTH = NOV,
  PAGES = {290--297},
  ADDRESS = {Dallas, TX},
  PUBLISHER = {IEEE Computer Society}
}


@ARTICLE{BlochingerSinzKuechlin03a,
  AUTHOR = {Wolfgang Blochinger and Carsten Sinz and Wolfgang K{\"u}chlin},
  TITLE = {Parallel Propositional Satisfiability Checking with Distributed
	Dynamic Learning},
  YEAR = 2003,
  JOURNAL = {Parallel Computing},
  VOLUME = 29,
  NUMBER = 7,
  PAGES = {969--994},
  PUBLISHER = {Elsevier}
}


@TECHREPORT{Sitaraman-etal:03,
  AUTHOR = {Murali Sitaraman and Durga P. Gandi and Wolfgang K{\"u}chlin
 		and Carsten Sinz and Bruce B. Weide},
  TITLE = {The Humane Bugfinder: Modular Static Analysis Using a {SAT}
		Solver},
  MONTH = JUN,
  YEAR = 2003,
  INSTITUTION = {Department of Computer Science, Clemson University, SC},
  NUMBER = {RSRG-03-05}
}


@INPROCEEDINGS{BlochingerSinzKuechlin03b,
  AUTHOR = {Wolfgang Blochinger and Carsten Sinz and Wolfgang K{\"u}chlin},
  TITLE = {A Universal Parallel {SAT} Checking Kernel},
  BOOKTITLE = {Proc.\ of the Intl.\ Conf.\ on Parallel and Distributed
	Processing Techniques and Applications ({PDPTA}'03)},
  MONTH = {June},
  ADDRESS = {Las Vegas, NV},
  PUBLISHER = {CSREA Press},
  EDITOR = {Hamid R. Arabnia and Youngsong Mun},
  VOLUME = 4,
  PAGES = {1720--1725},
  YEAR = 2003
}


@ARTICLE{SinzKaiserKuechlin:03,
  AUTHOR = {Carsten Sinz and Andreas Kaiser and Wolfgang K{\"u}chlin},
  TITLE = {Formal Methods for the Validation of Automotive Product
		Configuration Data},
  JOURNAL = {Artificial Intelligence for Engineering Design,
		Analysis and Manufacturing},
  PUBLISHER = {Cambridge University Press},
  VOLUME = 17,
  NUMBER = 1,
  PAGES = {75--97},
  YEAR = 2003,
  MONTH = JAN,
  NOTE = {Special issue on configuration.}
}


@ARTICLE{SinzLumppSchneiderKuechlin:02,
  AUTHOR = {Carsten Sinz and Thomas Lumpp and J{\"u}rgen Schneider
		and Wolfgang K{\"u}chlin},
  TITLE = {Detection of Dynamic Execution Errors in {IBM} {S}ystem
		{A}utomation's Rule-Based Expert System},
  JOURNAL = {Information and Software Technology},
  PUBLISHER = {Elsevier Science Publishers},
  VOLUME = 44,
  NUMBER = 14,
  YEAR = 2002,
  MONTH = NOV,
  PAGES = {857--873}
}


@INPROCEEDINGS{Sinz:02b,
  AUTHOR = {Carsten Sinz},
  TITLE = {Knowledge Compilation for Product Configuration},
  BOOKTITLE = {Configuration Workshop Proceedings, 15th European
		Conference on Artificial Intelligence ({ECAI}-2002)},
  YEAR = 2002,
  MONTH = JUL,
  ADDRESS = {Lyon, France},
  PAGES = {23--26}
}


@INPROCEEDINGS{DenzingerSinzAvenhausKuechlin:02,
  AUTHOR = {J{\"o}rg Denzinger and Carsten Sinz and
		J{\"u}rgen Avenhaus and Wolfgang K{\"u}chlin},
  TITLE = {{Teamwork-PaReDuX}: Knowledge-based Search with Multiple
		Parallel Agents},
  BOOKTITLE = {Proceedings of the International Conference on
		Massively Parallel Computing Systems ({MPCS 2002})},
  YEAR = 2002,
  MONTH = APR,
  ADDRESS = {Ischia, Italy},
  PUBLISHER = {National Technological University Press, Fort Collins, CO}
}


@INPROCEEDINGS{Sinz:02a,
  AUTHOR = {Carsten Sinz},
  TITLE = {Formal Verification in an Industrial Context},
  BOOKTITLE = {Symposium on the Effectiveness of Logic in Computer
		Science ({ELICS'02})},
  YEAR = 2002,
  MONTH = MAR,
  NOTE = {In Technical Report MPI-I-2002-2-007.},
  INSTITUTE = {Max Planck Institut f{\"u}r Informatik},
  PAGES = {59--63},
  ADDRESS = {Saarbr{\"u}cken, Germany}
}


@MISC{SinzSinz:02,
  AUTHOR = {Andrea Sinz and Carsten Sinz},
  TITLE = {Software Development for Determining Cross-Linking Sites
		in Proteins},
  MONTH = MAR,
  YEAR = 2002,
  HOWPUBLISHED = {Poster, 35. Diskussionstagung der Deutschen Gesellschaft
		f{\"u}r Massenspektrometrie ({DGMS 2002}), Heidelberg, Germany}
}


@INPROCEEDINGS{SinzLumppKuechlin:01,
  AUTHOR = {Carsten Sinz and Thomas Lumpp and Wolfgang K{\"u}chlin},
  TITLE = {Towards a Verification of the Rule-Based Expert System
		of the {IBM} {SA} for {OS/390} Automation Manager},
  BOOKTITLE = {Proceedings of the 2nd Asia-Pacific Conference on
		Quality Software ({APAQS 2001})},
  YEAR = 2001,
  MONTH = DEC,
  ADDRESS = {Hong Kong},
  PAGES = {367--374},
  PUBLISHER = {IEEE Computer Society}
}


@INPROCEEDINGS{SinzDenzingerAvenhausKuechlin:01,
  AUTHOR = {Carsten Sinz and J{\"o}rg Denzinger and J{\"u}rgen
		Avenhaus and Wolfgang K{\"u}chlin},
  TITLE = {Combining Parallel and Distributed Search in Automated
		Equational Deduction},
  BOOKTITLE = {Parallel Processing and Applied Mathematics {PPAM 2001}},
  YEAR = 2001,
  MONTH = SEP,
  ADDRESS = {Naleczow, Poland},
  SERIES = {LNCS},
  NUMBER = 2328,
  PUBLISHER = {Springer-Verlag}
}


@INPROCEEDINGS{BlochingerSinzKuechlin:01b,
  AUTHOR = {Wolfgang Blochinger and Carsten Sinz and
		Wolfgang K{\"u}chlin},
  TITLE = {Parallel Consistency Checking of Automotive Product Data},
  BOOKTITLE = {Proc.\ of Intl.\ Conference Parallel Computing
		({P}ar{C}o 2001)},
  YEAR = 2001,
  MONTH = SEP,
  ADDRESS = {Naples, Italy}
}


@INPROCEEDINGS{BlochingerSinzKuechlin:01a,
  AUTHOR = {Wolfgang Blochinger and Carsten Sinz and
		Wolfgang K{\"u}chlin},
  TITLE = {Distributed Parallel {SAT} Checking with Dynamic Learning
		using {DOTS}},
  EDITOR = {Gonzales, T.},
  BOOKTITLE = {Proc.\ of the IASTED Intl.\ Conference Parallel and
		Distributed Computing and Systems ({PDCS} 2001)},
  YEAR = 2001,
  PAGES = {396--401},
  MONTH = AUG,
  ADDRESS = {Anaheim, CA},
  PUBLISHER = {ACTA Press}
}


@INPROCEEDINGS{SinzKuechlin:01,
  AUTHOR = {Carsten Sinz and Wolfgang K{\"u}chlin},
  TITLE = {Dealing with Temporal Change in Product Documentation for
		Manufacturing},
  BOOKTITLE = {Configuration Workshop Proceedings, 17th International
		Joint Conference on Artificial Intelligence ({IJCAI-2001})},
  YEAR = 2001,
  MONTH = AUG,
  ADDRESS = {Seattle, WA},
  PAGES = {71--77}
}


@INPROCEEDINGS{SinzBlochingerKuechlin:01,
  AUTHOR = {Carsten Sinz and Wolfgang Blochinger and
		Wolfgang K{\"u}chlin},
  TITLE = {{PaSAT} - Parallel {SAT}-Checking with Lemma Exchange:
		Implementation and Applications},
  BOOKTITLE = {{LICS} 2001 Workshop on Theory and Applications of
		Satisfiability Testing ({SAT} 2001)},
  SERIES = {Electronic Notes in Discrete Mathematics},
  EDITOR = {Kautz, H. and Selman, B.},
  VOLUME = 9,
  ADDRESS = {Boston, MA},
  MONTH = JUN,
  YEAR = 2001,
  PUBLISHER = {Elsevier Science Publishers}
}


@INPROCEEDINGS{SinzKaiserKuechlin:01,
  AUTHOR = {Carsten Sinz and Andreas Kaiser and Wolfgang K{\"u}chlin},
  TITLE = {Detection of Inconsistencies in Complex Product
		Model Data Using Extended Propositional {SAT}-Checking},
  BOOKTITLE = {Proceedings of the 14th International {FLAIRS}
		Conference},
  EDITOR = {Russell, I. and Kolen, J.},
  PAGES = {645--649},
  MONTH = MAY,
  YEAR = 2001,
  PUBLISHER = {AAAI Press},
  ADDRESS = {Key West, FL}
}


@INPROCEEDINGS{SinzKaiserKuechlin:00,
  AUTHOR = {Carsten Sinz and Andreas Kaiser and Wolfgang K{\"u}chlin},
  TITLE = {{SAT}-Based Consistency Checking of Automotive Electronic
		Product Data},
  BOOKTITLE = {Configuration Workshop Proceedings, 14th European
		Conference on Artificial Intelligence ({ECAI}-2000)},
  YEAR = 2000,
  MONTH = AUG,
  PAGES = {74--78},
  ADDRESS = {Berlin, Germany}
}


@INPROCEEDINGS{Sinz:00,
  AUTHOR = {Carsten Sinz},
  TITLE = {System Description: {ARA} - An Automatic Theorem Prover
		for Relation Algebras},
  BOOKTITLE = {Automated Deduction {CADE-17}},
  EDITOR = {McAllester, D.},
  MONTH = JUN,
  YEAR = 2000,
  ADDRESS = {Pittsburgh, PA},
  SERIES = {LNAI},
  NUMBER = 1831,
  PAGES = {177--182},
  PUBLISHER = {Springer-Verlag}
}


@INPROCEEDINGS{SchimkatBlochingerSinzFriedrichKuechlin:00,
  AUTHOR = {Ralf-Dieter Schimkat and Wolfgang Blochinger and
		Carsten Sinz and Michael Friedrich and Wolfgang K{\"u}chlin},
  TITLE = {A Service-Based Agent Framework for Distributed Symbolic
        	Computation},
  BOOKTITLE = {Proc.\ 8th Intl.\ Conf.\ on High Performance Computing
        	and Networking Europe, {HPCN} 2000},
  EDITOR = {M. Bubak and R. Williams and H. Afsarmanesh and
		B. Hertzberger},
  PUBLISHER = {Springer-Verlag},
  SERIES = {LNCS},
  NUMBER = 1823,
  ADDRESS = {Amsterdam, Netherlands},
  MONTH = MAY,
  YEAR = 2000,
  PAGES = {644--656}
}


@INCOLLECTION{KuechlinSinz:00b,
  AUTHOR = {Wolfgang K{\"u}chlin and Carsten Sinz},
  TITLE = {Proving Consistency Assertions for 
                 Automotive Product Data Management},
  BOOKTITLE = {SAT2000 - Highlights of Satisfiability Research
		in the Year 2000},
  EDITOR = {I. Gent and H. van Maaren and T. Walsh},
  PUBLISHER = {IOS Press},
  YEAR = {2000},
  SERIES = {Frontiers in Artificial Intelligence and Applications},
  VOLUME = 63,
  PAGES = {}
}


@ARTICLE{KuechlinSinz:00a,
  AUTHOR = {Wolfgang K{\"u}chlin and Carsten Sinz},
  TITLE = {Proving Consistency Assertions for 
                 Automotive Product Data Management},
  JOURNAL = {J.\ Automated Reasoning},
  VOLUME = 24,
  NUMBER = {1--2},
  MONTH = FEB,
  YEAR = 2000,
  PAGES = {145--163},
  PUBLISHER = {Kluwer Academic Publishers}
}


@INPROCEEDINGS{BuendgenSinzWalter:96,
  AUTHOR = {Reinhard B{\"u}ndgen and Carsten Sinz and Jochen Walter},
  TITLE = {{ReDuX} 1.5: New Facets of Rewriting},
  BOOKTITLE = {Rewriting Techniques and Application {RTA-96}},
  EDITOR = {Harald Ganzinger},
  MONTH = JUL,
  YEAR = 1996,
  SERIES = {LNCS},
  NUMBER = 1103,
  PAGES = {412--415},
  PUBLISHER = {Springer-Verlag},
  ADDRESS = {New Brunswick, NJ}
}


@PHDTHESIS{Sinz:03,
  AUTHOR = {Carsten Sinz},
  TITLE = {{V}erifikation regelbasierter {K}onfigurationssysteme},
  SCHOOL = {Fakult{\"a}t f{\"u}r Informations- und Kognitionswissenschaften,
            Universit{\"a}t T{\"u}bingen},
  MONTH = DEC,
  YEAR = 2003,
  ADDRESS = {T{\"u}bingen, Germany}
}


@MASTERSTHESIS{Sinz:97b,
  AUTHOR = {Carsten Sinz},
  TITLE = {{B}aubarkeitspr{\"u}fung von {K}raftfahrzeugen durch
                automatisches {B}eweisen},
  SCHOOL = {Universit{\"a}t T{\"u}bingen},
  MONTH = DEC,
  YEAR = 1997,
  TYPE = {Diplomarbeit}
}


@MASTERSTHESIS{Sinz:97a,
  AUTHOR = {Carsten Sinz},
  TITLE = {{U}ntersuchung und {I}mplementation der {R}eduktionskalk{\"u}le
                RPC$_n$},
  SCHOOL = {Universit{\"a}t T{\"u}bingen},
  MONTH = JUN,
  YEAR = 1997,
  TYPE = {Studienarbeit}
}