Dr. rer. nat. Jörg Brauer

Contact

| | Email: brauer[at]embedded[dot]rwth-aachen[dot]de

Luck favors the prepared mind.
Louis Pasteur, 1822-1895

About me

I moved to Bremen.

Prior to moving up north, I used to be a PhD student heading the [mc]square project. [mc]square is a verification platform for microcontroller binary code. The key idea in [mc]square is to combine different formal methods in order to analyze hardware-specific microcontroller code. My own focus is the development of static analysis and abtract interpretation techniques specifically suited for verifying bit-twiddling programs. I am also involved in the CEVTES project, which is a joint project with the TU Vienna and the UAS Technikum Vienna on test-case generation for binary code.

Before I joined the Embedded Software Laboratory, I received my diploma degree from the Christian-Albrechts University of Kiel and visited NICTA in Sydney, Australia. At NICTA, I worked on Goanna, a static analyzer for the C/C++ programming languages.

See my CV for more details.

News

Research Interests

  • abstract interpretation of bit-vector programs (see [mc]square), in particular using automatic abstraction
  • relational abstract domains
  • formal verification
  • software model checking
  • software for embedded systems

In summary, I combine theoretical computer science with low-level programming, for example, by automatically deriving invariants for bit-twiddling binary code. I particularly enjoy utilizing SAT/SMT solvers for solving such problems. If you interested in this topic, you might want to check out my SAS'10 paper or my ESOP'11 paper, which give a good feel about how precise SAT-based abstract interpretation of bit-vector programs (such as assembly code) can get. However, to make such techniques scale, you need to apply certain other techniques, such as the projection algorithm from my CAV'11 paper.

Professional Activities

B.Sc./M.Sc./Diploma Theses

We always have a number of different topics for diploma, bachelors, and masters theses in the [mc]square project. Even though I do not supervise theses myself anymore, please contact me if you are interested in working on verification in the field of embedded software, preferably via email. We can probably find an interesting topic and a supervisor.

  • Ongoing
  • Finished
    • Na Bai (Diploma): Dataflow Analysis for PLCs (September 2011)
    • Sebastian Biallas (Diploma): Counterexample-Guided Abstraction Refinement for Programmable Logic Controllers (April 2010)
    • Frank Birbacher (Diploma): Relational Static Analysis of IL-Programs using Congruences
    • Lucas Brutschy (B.Sc.): Static Analysis of Microcontroller Software using SAT- and Constraint-Solving (August 2009)
    • Mustafa Karafil (Diploma): Recovering Indirect Control Flow in Binary Code (August 2011)
    • Jörg Toborg (Diploma): Static Analysis for the Renesas R8C/23 Tiny Microcontroller (February 2010)

Publications

A more detailed list of my publications can be found here (including abstracts), and a list of my co-authors can be found here.


Publikations-Export
[RBH+14]
Reinbacher, T., Brauer, J., Horauer, M., Steininger, A., and Kowalewski, S., "Runtime verification of microcontroller binary code", Science of computer programming, vol. 80, pp. 109-129, 2014

Runtime verification of microcontroller binary code

Bibtex entry :

@article {  RBH+14,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Steininger, Andreas and Kowalewski, Stefan },
	title = { Runtime verification of microcontroller binary code },
	journal = { Science of computer programming },
	publisher = { Elsevier },
	pages = { 109-129 },
	volume = { 80 },
	year = { 2014 },
	address = { Amsterdam },
	issn = { 0167-6423 },
	doi = { 10.1016/j.scico.2012.10.015 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-080463 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/231479 },
}
[RFB14]
Reinbacher, T., Fuegger, M., and Brauer, J., "Runtime verification of embedded real-time systems", Formal methods in system design, vol. 44, iss. 3, pp. 203-239, 2014

Runtime verification of embedded real-time systems

Bibtex entry :

@article {  RFB14,
	author = { Reinbacher, Thomas and Fuegger, Matthias and Brauer,
		J{\"o}rg },
	title = { Runtime verification of embedded real-time systems },
	journal = { Formal methods in system design },
	publisher = { Springer Science + Business Media B.V },
	pages = { 203-239 },
	volume = { 44 },
	number = { 3 },
	year = { 2014 },
	address = { Dordrecht },
	issn = { 0925-9856 },
	doi = { 10.1007/s10703-013-0199-z },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-089599 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/446689 },
}
[BK13]
Brauer, J. and Kowalewski, S., "Automatic abstraction for bit vectors using decision procedures", , Aachen, AIB 2013 14, 2013.

Automatic abstraction for bit vectors using decision procedures

Bibtex entry :

@techreport {  BK13,
	author = { Brauer, J{\"o}rg and Kowalewski, Stefan },
	title = { Automatic abstraction for bit vectors using decision
		procedures },
	publisher = { Fachgruppe Informatik, RWTH Aachen University },
	pages = { IV, 207 S. : graph. Darst. },
	volume = { 2013,14 },
	number = { AIB 2013 14 },
	series = { Aachener Informatik-Berichte },
	year = { 2013 },
	address = { Aachen },
	typ = { PUB:(DE-HGF)11 },
	reportid = { RWTH-CONV-010470 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/229199/files/4836.pdf },
}
[BKK13]
Brauer, J., King, A., and Kowalewski, S., "Abstract interpretation of microcontroller code: Intervals meet congruences", Science of computer programming, vol. 78, iss. 7, pp. 862-883, 2013

Abstract interpretation of microcontroller code: Intervals meet congruences

Bibtex entry :

@article {  BKK13,
	author = { Brauer, J{\"o}rg and King, Andy and Kowalewski, Stefan },
	title = { Abstract interpretation of microcontroller code: Intervals
		meet congruences },
	journal = { Science of computer programming },
	publisher = { Elsevier },
	pages = { 862-883 },
	volume = { 78 },
	number = { 7 },
	year = { 2013 },
	address = { Amsterdam [u.a.] },
	issn = { 0167-6423 },
	doi = { 10.1016/j.scico.2012.06.001 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-086725 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/238031 },
}
[KPB13]
Kowalewski, S., Philippou, A., and Brauer, J., "Model checking and abstract interpretation as building blocks of advanced program analysis techniques", International Journal on Software Tools for Technology Transfer, vol. 15, iss. 4, pp. 287-289, 2013

Model checking and abstract interpretation as building blocks of advanced program analysis techniques

Bibtex entry :

@article {  KPB13,
	author = { Kowalewski, S. and Philippou, A. and Brauer, J. },
	title = { Model checking and abstract interpretation as building
		blocks of advanced program analysis techniques },
	journal = { International Journal on Software Tools for Technology
		Transfer },
	publisher = { Springer Science & Business Media },
	pages = { 287-289 },
	volume = { 15 },
	number = { 4 },
	year = { 2013 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-236324 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752289 },
}
[BBK+12]
Biallas, S., Brauer, J., King, A., and Kowalewski, S., "Loop Leaping with Closures", in Proc. 19th Static Analysis Symposium, 2012 in Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 214-230.

Loop Leaping with Closures

Bibtex entry :

@inproceedings {  BBK+12,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and King, Andy and
		Kowalewski, Stefan },
	title = { Loop Leaping with Closures },
	booktitle = { 19th Static Analysis Symposium },
	publisher = { Springer Berlin Heidelberg },
	pages = { 214-230 },
	series = { Lecture Notes in Computer Science },
	year = { 2012 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-236335 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752305 },
}
[BBK12a]
Beckschulze, E., Brauer, J., and Kowalewski, S., "Access-Based Localization for Octagons", Electronic notes in theoretical computer science : ENTCS, vol. 287, pp. 29-40, 2012

Access-Based Localization for Octagons

Bibtex entry :

@article {  BBK12a,
	author = { Beckschulze, Eva and Brauer, J{\"o}rg and Kowalewski, Stefan },
	title = { Access-Based Localization for Octagons },
	journal = { Electronic notes in theoretical computer science : ENTCS },
	publisher = { Elsevier Science },
	pages = { 29-40 },
	volume = { 287 },
	year = { 2012 },
	address = { Amsterdam [u.a.] },
	issn = { 1571-0661 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-043099 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/165238 },
}
[BBK12b]
Biallas, S., Brauer, J., and Kowalewski, S., "Arcade.PLC : a Verification Platform for Programmable Logic Controllers", in Proc. 2012 proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE 2012) : Essen, Germany, 3 - 7 September 2012, Piscataway, NJ, 2012, IEEE, pp. 338-341.

Arcade.PLC : a Verification Platform for Programmable Logic Controllers

Bibtex entry :

@inproceedings {  BBK12b,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
		Stefan },
	title = { Arcade.PLC : a Verification Platform for Programmable Logic
		Controllers },
	booktitle = { 2012 proceedings of the 27th IEEE/ACM International
		Conference on Automated Software Engineering (ASE 2012) :
		Essen, Germany, 3 - 7 September 2012 },
	publisher = { IEEE },
	pages = { 338-341 },
	year = { 2012 },
	address = { Piscataway, NJ },
	doi = { 10.1145/2351676.2351741 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-170936 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/97761 },
}
[BHK+12]
Brauer, J., Hansen, R. R., Kowalewski, S., Larsen, K. G., and Olesen, M. C., "Adaptable Value-Set Analysis for Low-Level Code", in Proc. 6th International Workshop on Systems Software Verification (SSV 2011) [Elektronische Ressource] / Hrsg.: Jörg Brauer ; Marco Roveri ; Hendrik Tews, Wadern, 2012 in OASIcs - OpenAccess Series in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 32-43.

Adaptable Value-Set Analysis for Low-Level Code

Bibtex entry :

@inproceedings {  BHK+12,
	author = { Brauer, J{\"o}rg and Hansen, Rene Rydhof and Kowalewski,
		Stefan and Larsen, Kim G. and Olesen, Mads Chr. },
	title = { Adaptable Value-Set Analysis for Low-Level Code },
	booktitle = { 6th International Workshop on Systems Software Verification
		(SSV 2011) [Elektronische Ressource] / Hrsg.: J{\"o}rg
		Brauer ; Marco Roveri ; Hendrik Tews },
	publisher = { Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik },
	pages = { 32-43 },
	series = { OASIcs - OpenAccess Series in Informatics },
	year = { 2012 },
	address = { Wadern },
	doi = { 10.4230/OASIcs.SSV.2011.32 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-198838 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/128784 },
}
[BK12a]
Brauer, J. and King, A., "Transfer function synthesis without quantifier elimination", Logical methods in computer science : LMCS, vol. 8, iss. 3, 2012

Transfer function synthesis without quantifier elimination

Bibtex entry :

@article {  BK12a,
	author = { Brauer, J{\"o}rg and King, Andy },
	title = { Transfer function synthesis without quantifier elimination },
	journal = { Logical methods in computer science : LMCS },
	publisher = { Department of Theoretical Computer Science, TU [u.a.] },
	volume = { 8 },
	number = { 3 },
	year = { 2012 },
	address = { Braunschweig },
	issn = { 1860-5974 },
	doi = { 10.2168/LMCS-8(3:17)2012 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-079893 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/218122/files/218122.pdf },
}
[BS12]
Brauer, J. and Simon, A., "Inferring Definite Counterexamples Through Under-Approximation", in Proc. NASA formal methods : 4th international symposium, NFM 2012, Norfolk, VA, USA, April 3 - 5, 2012 ; proceedings / Alwyn E. Goodloe; Suzette Person (ed.), Berlin ; Heidelberg [u.a.], 2012 in Lecture Notes in Computer Science, Springer, pp. 54-69.

Inferring Definite Counterexamples Through Under-Approximation

Bibtex entry :

@inproceedings {  BS12,
	author = { Brauer, J{\"o}rg and Simon, Axel },
	title = { Inferring Definite Counterexamples Through
		Under-Approximation },
	booktitle = { NASA formal methods : 4th international symposium, NFM 2012,
		Norfolk, VA, USA, April 3 - 5, 2012 ; proceedings / Alwyn E.
		Goodloe; Suzette Person (ed.) },
	publisher = { Springer },
	pages = { 54-69 },
	series = { Lecture Notes in Computer Science },
	year = { 2012 },
	address = { Berlin ; Heidelberg [u.a.] },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194497 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/123648 },
}
[BSK12]
Brauer, J., Schlich, B., and Kowalewski, S., "Parallel and distributed invariant checking of microcontroller software", Electronic notes in theoretical computer science : ENTCS, vol. 287, pp. 45-63, 2012

Parallel and distributed invariant checking of microcontroller software

Bibtex entry :

@article {  BSK12,
	author = { Brauer, J{\"o}rg and Schlich, Bastian and Kowalewski, Stefan },
	title = { Parallel and distributed invariant checking of
		microcontroller software },
	journal = { Electronic notes in theoretical computer science : ENTCS },
	publisher = { Elsevier Science },
	pages = { 45-63 },
	volume = { 287 },
	year = { 2012 },
	address = { Amsterdam [u.a.] },
	issn = { 1571-0661 },
	doi = { 10.1016/j.entcs.2009.09.059 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-013643 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/132534 },
}
[BBK+11]
Biallas, S., Brauer, J., Kowalewski, S., and Schlich, B., "Automatically Deriving Symbolic Invariants for PLC Programs Written in IL", in Proc. Formal methods for automation and safety in railway and automotive systems : FORMS/FORMAT 2010 ; [8th symposium ; proceedings] / Eckehard Schnieder; Géza Tarnai, eds., Heidelberg [u.a.], 2011, Springer, pp. 237-245.

Automatically Deriving Symbolic Invariants for PLC Programs Written in IL

Bibtex entry :

@inproceedings {  BBK+11,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
		Stefan and Schlich, Bastian },
	title = { Automatically Deriving Symbolic Invariants for PLC Programs
		Written in IL },
	booktitle = { Formal methods for automation and safety in railway and
		automotive systems : FORMS/FORMAT 2010 ; [8th symposium ;
		proceedings] / Eckehard Schnieder; Géza Tarnai, eds. },
	publisher = { Springer },
	pages = { 237-245 },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-14261-1 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196797 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/126461 },
}
[BBK11]
Biallas, S., Brauer, J., and Kowalewski, S., "SAT-Based Abstraction Refinement for Programmable Logic Controllers", in Proc. 3rd International Workshop on Dependable Control of Discrete Systems 2011, DCDS 2011, Saarbrücken, Germany, 15th-17theJune 2011, Piscataway, NJ, 2011, IEEE, pp. 96-101.

SAT-Based Abstraction Refinement for Programmable Logic Controllers

Bibtex entry :

@inproceedings {  BBK11,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
		Stefan },
	title = { SAT-Based Abstraction Refinement for Programmable Logic
		Controllers },
	booktitle = { 3rd International Workshop on Dependable Control of Discrete
		Systems 2011, DCDS 2011, Saarbr{\"u}cken, Germany,
		15th-17theJune 2011 },
	publisher = { IEEE },
	pages = { 96-101 },
	year = { 2011 },
	address = { Piscataway, NJ },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194508 },
	cin = { 122810 / 120000 },
	url = { http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=05970325 },
}
[BBS+11]
Beckschulze, E., Brauer, J., Stollenwerk, A., and Kowalewski, S., "Analyzing Embedded Systems Code for Mixed-Critical Systems Using Hybrid Memory Representations", in Proc. 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing workshops (ISORCW) : 28 - 31 March 2011, Newport Beach, California, USA ; proceedings, Piscataway, NJ, 2011, IEEE, pp. 33-40.

Analyzing Embedded Systems Code for Mixed-Critical Systems Using Hybrid Memory Representations

Bibtex entry :

@inproceedings {  BBS+11,
	author = { Beckschulze, Eva and Brauer, J{\"o}rg and Stollenwerk,
		André and Kowalewski, Stefan },
	title = { Analyzing Embedded Systems Code for Mixed-Critical Systems
		Using Hybrid Memory Representations },
	booktitle = { 2011 14th IEEE International Symposium on
		Object/Component/Service-Oriented Real-Time Distributed
		Computing workshops (ISORCW) : 28 - 31 March 2011, Newport
		Beach, California, USA ; proceedings },
	publisher = { IEEE },
	pages = { 33-40 },
	year = { 2011 },
	address = { Piscataway, NJ },
	organization = { 14th IEEE International Symposium on
		Object/Component/Service-Oriented Real-Time Distributed
		Computing, Newport Beach, CA (USA), 2011-03-28 - 2011-08-31 },
	doi = { 10.1109/ISORCW.2011.40 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-194737 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/124002 },
}
[BK11]
Brauer, J. and King, A., "Approximate Quantifier Elimination for Propositional Boolean Formulae", in Proc. NASA formal methods : third international symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011 ; proceedings / Mihaela Bobaru ... (eds.), Heidelberg [u.a.], 2011 in Lecture Notes in Computer Science, Springer, pp. 73-88.

Approximate Quantifier Elimination for Propositional Boolean Formulae

Bibtex entry :

@inproceedings {  BK11,
	author = { Brauer, J{\"o}rg and King, Andy },
	title = { Approximate Quantifier Elimination for Propositional Boolean
		Formulae },
	booktitle = { NASA formal methods : third international symposium, NFM
		2011, Pasadena, CA, USA, April 18-20, 2011 ; proceedings /
		Mihaela Bobaru ... (eds.) },
	publisher = { Springer },
	pages = { 73-88 },
	series = { Lecture Notes in Computer Science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-20398-5 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194773 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/124043 },
}
[BK11a]
Brauer, J. and King, A., "Transfer Function Synthesis without Quantifier Elimination", in Proc. Programming languages and systems : 20th European Symposium on Programming, ESOP 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011 ; proceedings / Gilles Barthe (ed.), Heidelberg [u.a.], 2011 in Lecture notes in computer science, Springer, pp. 97-115.

Transfer Function Synthesis without Quantifier Elimination

Bibtex entry :

@inproceedings {  BK11a,
	author = { Brauer, J{\"o}rg and King, Andy },
	title = { Transfer Function Synthesis without Quantifier Elimination },
	booktitle = { Programming languages and systems : 20th European Symposium
		on Programming, ESOP 2011, held as part of the Joint
		European Conference on Theory and Practice of Software,
		ETAPS 2011, Saarbr{\"u}cken, Germany, March 26-April 3, 2011
		; proceedings / Gilles Barthe (ed.) },
	publisher = { Springer },
	pages = { 97-115 },
	series = { Lecture notes in computer science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-19718-5 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196794 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/126458 },
}
[BKK11]
Brauer, J., King, A., and Kriener, J., "Existential Quantification as Incremental SAT", in Proc. Computer aided verification : 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011 ; proceedings / Ganesh Gopalakrishnan; Shaz Qadeer (eds.), Heidelberg [u.a.], 2011 in Lecture notes in computer science, Springer, pp. 191-207.

Existential Quantification as Incremental SAT

Bibtex entry :

@inproceedings {  BKK11,
	author = { Brauer, J{\"o}rg and King, Andy and Kriener, Jael },
	title = { Existential Quantification as Incremental SAT },
	booktitle = { Computer aided verification : 23rd international conference,
		CAV 2011, Snowbird, UT, USA, July 14-20, 2011 ; proceedings
		/ Ganesh Gopalakrishnan; Shaz Qadeer (eds.) },
	publisher = { Springer },
	pages = { 191-207 },
	series = { Lecture notes in computer science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-22110-1 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196588 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/126209 },
}
[BRT11]
Brauer, J., Roveri, M., and Tews, H., "Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011)", , Dresden, TUD–FI11–02–August 2011, 2011.

Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011)

Bibtex entry :

@techreport {  BRT11,
	author = { Brauer, J{\"o}rg and Roveri, Marco and Tews, Hendrik },
	title = { Proceedings of the 6th International Workshop on Systems
		Software Verification (SSV 2011) },
	publisher = { TU },
	pages = { 101 S. },
	number = { TUD–FI11–02–August 2011 },
	year = { 2011 },
	address = { Dresden },
	typ = { PUB:(DE-HGF)26 },
	reportid = { RWTH-CONV-008161 },
	cin = { 122810 / 120000 },
	url = { https://es.fbk.eu/events/ssv2011/papers/proceedings.pdf },
}
[RB11]
Reinbacher, T. and Brauer, J., "Precise Control Flow Reconstruction Using Boolean Logic", in Proc. EMSOFT '11 : Proceedings of the ninth ACM international conference on Embedded software ; October 9-14, 2011, Taipei, Taiwan, New York, NY, 2011, ACM, pp. 117-126.

Precise Control Flow Reconstruction Using Boolean Logic

Bibtex entry :

@inproceedings {  RB11,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg },
	title = { Precise Control Flow Reconstruction Using Boolean Logic },
	booktitle = { EMSOFT '11 : Proceedings of the ninth ACM international
		conference on Embedded software ; October 9-14, 2011,
		Taipei, Taiwan },
	publisher = { ACM },
	pages = { 117-126 },
	year = { 2011 },
	address = { New York, NY },
	doi = { 10.1145/2038642.2038662 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-198496 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/128379 },
}
[RBH+11]
Reinbacher, T., Brauer, J., Horauer, M., Steininger, A., and Kowalewski, S., "Past Time LTL Runtime Verification for Microcontroller Binary Code", in Proc. Formal methods for industrial critical systems : 16th international workshop, FMICS 2011, Trento, Italy, August 29 - 30, 2011 ; proceedings / Gwen Salaün; Bernhard Schätz (eds.), Heidelberg [u.a.], 2011 in Lecture notes in computer science, Springer, pp. 37-51.

Past Time LTL Runtime Verification for Microcontroller Binary Code

Bibtex entry :

@inproceedings {  RBH+11,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Steininger, Andreas and Kowalewski, Stefan },
	title = { Past Time LTL Runtime Verification for Microcontroller
		Binary Code },
	booktitle = { Formal methods for industrial critical systems : 16th
		international workshop, FMICS 2011, Trento, Italy, August 29
		- 30, 2011 ; proceedings / Gwen Sala{\"u}n; Bernhard
		Sch{\"a}tz (eds.) },
	publisher = { Springer },
	pages = { 37-51 },
	series = { Lecture notes in computer science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-24431-5 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194606 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/123834 },
}
[RBS+11]
Reinbacher, T., Brauer, J., Schachinger, D., Steininger, A., and Kowalewski, S., "Automated Test-Trace Inspection for Microcontroller Binary Code", in Proc. Runtime Verification : Second International Conference, RV 2011, San Francisco, CA, USA, September 27-30, 2011, Revised Selected Papers / edited by Sarfraz Khurshid, Koushik Sen, Berlin ; Heidelberg, 2011 in Lecture notes in computer science, Springer, pp. 239-244.

Automated Test-Trace Inspection for Microcontroller Binary Code

Bibtex entry :

@inproceedings {  RBS+11,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Schachinger,
		Daniel and Steininger, Andreas and Kowalewski, Stefan },
	title = { Automated Test-Trace Inspection for Microcontroller Binary
		Code },
	booktitle = { Runtime Verification : Second International Conference, RV
		2011, San Francisco, CA, USA, September 27-30, 2011, Revised
		Selected Papers / edited by Sarfraz Khurshid, Koushik Sen },
	publisher = { Springer },
	pages = { 239-244 },
	series = { Lecture notes in computer science },
	year = { 2011 },
	address = { Berlin ; Heidelberg },
	doi = { 10.1007/978-3-642-29860-8_18 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194496 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/123647 },
}
[RHS+11]
Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., and Scheuer, F., "Model checking embedded software of an industrial knitting machine", International journal of information technology, communications and convergence, vol. 1, iss. 2, pp. 186-205, 2011

Model checking embedded software of an industrial knitting machine

Bibtex entry :

@article {  RHS+11,
	author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
		and Brauer, J{\"o}rg and Scheuer, Florian },
	title = { Model checking embedded software of an industrial knitting
		machine },
	journal = { International journal of information technology,
		communications and convergence },
	publisher = { Inderscience Publishers },
	pages = { 186-205 },
	volume = { 1 },
	number = { 2 },
	year = { 2011 },
	address = { Geneva },
	issn = { 2042-3217 },
	doi = { 10.1504/IJITCC.2011.039285 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-052838 },
	cin = { 122810 / 120000 },
	url = { http://www.inderscience.com/IJITCC },
}
[RSM+11]
Reinbacher, T., Steininger, A., Müller, T., Horauer, M., Brauer, J., and Kowalewski, S., "Hardware Support for Efficient Testing of Embedded Software", in Proc. Proceedings of the ASME International Design Engineering Technical Conferences and Computers and Information in Engineering Conference - 2011 : presented at ASME 2011 International Design Engineering Technical Conferences and Computers and Information in Engineering Conference, August 28 - 31, 2011, Washington, D.C. / sponsored by the Design Engineering Division, ASME; the Computers and Information in Engineering Division, ASME. - Vol. 3: ASME/IEEE International Conference on Mechatronic and Embedded Systems and Applications, Pt. A, New York, NY, 2011, ASME, pp. 3-12.

Hardware Support for Efficient Testing of Embedded Software

Bibtex entry :

@inproceedings {  RSM+11,
	author = { Reinbacher, Thomas and Steininger, Andreas and M{\"u}ller,
		Tobias and Horauer, Martin and Brauer, J{\"o}rg and
		Kowalewski, Stefan },
	title = { Hardware Support for Efficient Testing of Embedded Software },
	booktitle = { Proceedings of the ASME International Design Engineering
		Technical Conferences and Computers and Information in
		Engineering Conference - 2011 : presented at ASME 2011
		International Design Engineering Technical Conferences and
		Computers and Information in Engineering Conference, August
		28 - 31, 2011, Washington, D.C. / sponsored by the Design
		Engineering Division, ASME; the Computers and Information in
		Engineering Division, ASME. - Vol. 3: ASME/IEEE
		International Conference on Mechatronic and Embedded Systems
		and Applications, Pt. A },
	publisher = { ASME },
	pages = { 3-12 },
	year = { 2011 },
	address = { New York, NY },
	doi = { 10.1115/DETC2011-47139 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-195986 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/125522 },
}
[SBK11]
Schlich, B., Brauer, J., and Kowalewski, S., "Application of Static Analyses for State-Space Reduction to the Microcontroller Binary Code", Science of computer programming, vol. 76, iss. 2, pp. 100-118, 2011

Application of Static Analyses for State-Space Reduction to the Microcontroller Binary Code

Bibtex entry :

@article {  SBK11,
	author = { Schlich, Bastian and Brauer, J{\"o}rg and Kowalewski, Stefan },
	title = { Application of Static Analyses for State-Space Reduction to
		the Microcontroller Binary Code },
	journal = { Science of computer programming },
	publisher = { Elsevier },
	pages = { 100-118 },
	volume = { 76 },
	number = { 2 },
	year = { 2011 },
	address = { Amsterdam [u.a.] },
	issn = { 0167-6423 },
	doi = { 10.1016/j.scico.2010.03.006 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-062661 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/186222 },
}
[SNB+11]
Schlich, B., Noll, T., Brauer, J., and Brutschy, L., "Reduction of Interrupt Handler Executions for Model Checking Embedded Software", in Proc. Hardware and software: verification and testing : 5th International Haifa Verification Conference, HCV 2009, Haifa, Israel, October 19-22, 2009 : revised selected papers / Kedar Namjoshi ... (eds.), Heidelberg [u.a.], 2011 in Lecture Notes in Computer Science, Springer.

Reduction of Interrupt Handler Executions for Model Checking Embedded Software

Bibtex entry :

@inproceedings {  SNB+11,
	author = { Schlich, Bastian and Noll, Thomas and Brauer, J{\"o}rg and
		Brutschy, Lucas },
	title = { Reduction of Interrupt Handler Executions for Model Checking
		Embedded Software },
	booktitle = { Hardware and software: verification and testing : 5th
		International Haifa Verification Conference, HCV 2009,
		Haifa, Israel, October 19-22, 2009 : revised selected papers
		/ Kedar Namjoshi ... (eds.) },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-19237-1_5 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-187757 },
	cin = { 122810 / 121310 / 120000 },
	url = { http://publications.rwth-aachen.de/record/116214 },
}
[BBG+10]
Biallas, S., Brauer, J., Gückel, D., and Kowalewski, S., "On-The-Fly Path Reduction", in Proc. 4th International Workshop on Harnessing Theories for Tool Support in Software : TTSS’10 ; East China Normal University, Shanghai, China, November 15, 2010 ; Preliminary Proceedings / Eds.: Min Zhang and Volker Stolz, Macau, 2010 in UNU-IIST Report, UNU-IIST, pp. 108-122.

On-The-Fly Path Reduction

Bibtex entry :

@inproceedings {  BBG+10,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and G{\"u}ckel,
		Dominique and Kowalewski, Stefan },
	title = { On-The-Fly Path Reduction },
	booktitle = { 4th International Workshop on Harnessing Theories for Tool
		Support in Software : TTSS’10 ; East China Normal
		University, Shanghai, China, November 15, 2010 ; Preliminary
		Proceedings / Eds.: Min Zhang and Volker Stolz },
	publisher = { UNU-IIST },
	pages = { 108-122 },
	series = { UNU-IIST Report },
	year = { 2010 },
	address = { Macau },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190152 },
	cin = { 122810 / 120000 },
	url = { http://i.unu.edu/unu/u/publication/000/001/286/report444.pdf },
}
[BBK10]
Biallas, S., Brauer, J., and Kowalewski, S., "Counterexample-Guided Abstraction Refinement for PLCs", in Proc. 5th International Workshop on Systems Software Verification (SSV 2010), Vancouver, Canada, 2010.

Counterexample-Guided Abstraction Refinement for PLCs

Bibtex entry :

@inproceedings {  BBK10,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
		Stefan },
	title = { Counterexample-Guided Abstraction Refinement for PLCs },
	booktitle = { 5th International Workshop on Systems Software Verification
		(SSV 2010), Vancouver, Canada },
	year = { 2010 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-189856 },
	cin = { 122810 / 120000 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbk10.pdf },
}
[BK10]
Brauer, J. and King, A., "Automatic Abstraction for Intervals using Boolean Formulae", in Proc. Static analysis : 17th international symposium, SAS 2010, Perpignan, France, September 14-16, 2010 ; proceedings / Radhia Cousot; Matthieu Martel (eds.), Berlin [u.a.], 2010 in Lecture notes in computer science, Springer, pp. 167-183.

Automatic Abstraction for Intervals using Boolean Formulae

Bibtex entry :

@inproceedings {  BK10,
	author = { Brauer, J{\"o}rg and King, Andy },
	title = { Automatic Abstraction for Intervals using Boolean Formulae },
	booktitle = { Static analysis : 17th international symposium, SAS 2010,
		Perpignan, France, September 14-16, 2010 ; proceedings /
		Radhia Cousot; Matthieu Martel (eds.) },
	publisher = { Springer },
	pages = { 167-183 },
	series = { Lecture notes in computer science },
	year = { 2010 },
	address = { Berlin [u.a.] },
	doi = { 10.1007/978-3-642-15769-1_11 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190302 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/119140 },
}
[BKK+10]
Brauer, J., Kamin, V., Kowalewski, S., and Noll, T., "Loop Refinement using Octagons and Satisfiability", in Proc. SSV'10 : Proceedings of the 5th international conference on Systems software verification, New York, NY, 2010, ACM, p. 9.

Loop Refinement using Octagons and Satisfiability

Bibtex entry :

@inproceedings {  BKK+10,
	author = { Brauer, J{\"o}rg and Kamin, Volker and Kowalewski, Stefan
		and Noll, Thomas },
	title = { Loop Refinement using Octagons and Satisfiability },
	booktitle = { SSV'10 : Proceedings of the 5th international conference on
		Systems software verification },
	publisher = { ACM },
	pages = { 9 S. },
	year = { 2010 },
	address = { New York, NY },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196798 },
	cin = { 122810 / 121310 / 120000 },
	url = { http://dl.acm.org/citation.cfm?id=1929004&picked=prox },
}
[BKK10]
Brauer, J., King, A., and Kowalewski, S., "Range Analysis of Microcontroller Code using Bit-Level Congruences", in Proc. Formal methods for industrial critical systems : 15th international workshop, FMICS 2010, Antwerp, Belgium, September 20 - 21, 2010 ; proceedings / Stefan Kowalewski; Marco Roveri (eds.), Berlin [u.a.], 2010 in Lecture notes in computer science, Springer, pp. 82-98.

Range Analysis of Microcontroller Code using Bit-Level Congruences

Bibtex entry :

@inproceedings {  BKK10,
	author = { Brauer, J{\"o}rg and King, Andy and Kowalewski, Stefan },
	title = { Range Analysis of Microcontroller Code using Bit-Level
		Congruences },
	booktitle = { Formal methods for industrial critical systems : 15th
		international workshop, FMICS 2010, Antwerp, Belgium,
		September 20 - 21, 2010 ; proceedings / Stefan Kowalewski;
		Marco Roveri (eds.) },
	publisher = { Springer },
	pages = { 82-98 },
	series = { Lecture notes in computer science },
	year = { 2010 },
	address = { Berlin [u.a.] },
	doi = { 10.1007/978-3-642-15898-8_6 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190303 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/119141 },
}
[BNS10]
Brauer, J., Noll, T., and Schlich, B., "Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software", in Proc. SCOPES '10 Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems : St. Goar, Germany - June 29-30, 2010, New York, NY, 2010 in ACM Digital Library, ACM.

Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software

Bibtex entry :

@inproceedings {  BNS10,
	author = { Brauer, J{\"o}rg and Noll, Thomas and Schlich, Bastian },
	title = { Interval Analysis of Microcontroller Code using Abstract
		Interpretation of Hardware and Software },
	booktitle = { SCOPES '10 Proceedings of the 13th International Workshop on
		Software & Compilers for Embedded Systems : St. Goar,
		Germany - June 29-30, 2010 },
	publisher = { ACM },
	series = { ACM Digital Library },
	year = { 2010 },
	address = { New York, NY },
	doi = { 10.1145/1811212.1811216 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-191119 },
	cin = { 122810 / 121310 / 120000 },
	url = { http://publications.rwth-aachen.de/record/120063 },
}
[GBK10]
Gückel, D., Brauer, J., and Kowalewski, S., "A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification", in Proc. 2010 International Symposium on Industrial Embedded Systems (SIES 2010) : Trento, Italy, 7 - 9 July 2010 / [University of Trento, Italy; IEEE; IES], Piscataway, NJ, 2010, IEEE, pp. 118-127.

A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification

Bibtex entry :

@inproceedings {  GBK10,
	author = { G{\"u}ckel, Dominique and Brauer, J{\"o}rg and Kowalewski,
		Stefan },
	title = { A System for Synthesizing Abstraction-Enabled Simulators for
		Binary Code Verification },
	booktitle = { 2010 International Symposium on Industrial Embedded Systems
		(SIES 2010) : Trento, Italy, 7 - 9 July 2010 / [University
		of Trento, Italy; IEEE; IES] },
	publisher = { IEEE },
	pages = { 118-127 },
	year = { 2010 },
	address = { Piscataway, NJ },
	doi = { 10.1109/SIES.2010.5551382 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190384 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/119226 },
}
[GSB+10]
Gückel, D., Schlich, B., Brauer, J., and Kowalewski, S., "Synthesizing Simulators for Model Checking Microcontroller Binary", in Proc. Proceedings of the 13th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems : April 14–16, 2010, Vienna, Austria / Sponsored by IEEE Computer Society, Test Technology Techn. Council, In coop. with Dept. of Computer Engineering, Fac. of Informatics, Vienna Univ. of Techn., Piscataway, NJ, 2010, IEEE, pp. 313-316.

Synthesizing Simulators for Model Checking Microcontroller Binary

Bibtex entry :

@inproceedings {  GSB+10,
	author = { G{\"u}ckel, Dominique and Schlich, Bastian and Brauer,
		J{\"o}rg and Kowalewski, Stefan },
	title = { Synthesizing Simulators for Model Checking Microcontroller
		Binary },
	booktitle = { Proceedings of the 13th IEEE Symposium on Design and
		Diagnostics of Electronic Circuits and Systems : April
		14–16, 2010, Vienna, Austria / Sponsored by IEEE Computer
		Society, Test Technology Techn. Council, In coop. with Dept.
		of Computer Engineering, Fac. of Informatics, Vienna Univ.
		of Techn. },
	publisher = { IEEE },
	pages = { 313-316 },
	year = { 2010 },
	address = { Piscataway, NJ },
	doi = { 10.1109/DDECS.2010.5491761 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190385 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/119227 },
}
[RBH+10]
Reinbacher, T., Brauer, J., Horauer, M., Steininger, A., and Kowalewski, S., "Test-Case Generation for Embedded Binary Code Using Abstract Interpretation", in Proc. Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (Selected Papers) (MEMICS 2010) [Elektronische Ressource] / Hrsg.: Ludek Matyska ; Michal Kozubek ; Tomáš Vojnar ; Pavel Zemcík ; David Antos, Wadern, 2010 in OASIcs - OpenAccess Series in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 101-108.

Test-Case Generation for Embedded Binary Code Using Abstract Interpretation

Bibtex entry :

@inproceedings {  RBH+10,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Steininger, Andreas and Kowalewski, Stefan },
	title = { Test-Case Generation for Embedded Binary Code Using Abstract
		Interpretation },
	booktitle = { Sixth Doctoral Workshop on Mathematical and Engineering
		Methods in Computer Science (Selected Papers) (MEMICS 2010)
		[Elektronische Ressource] / Hrsg.: Ludek Matyska ; Michal
		Kozubek ; Tomáš Vojnar ; Pavel Zemcík ; David Antos },
	publisher = { Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik },
	pages = { 101-108 },
	series = { OASIcs - OpenAccess Series in Informatics },
	year = { 2010 },
	address = { Wadern },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196795 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/126459 },
}
[RHS+10]
Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., and Scheuer, F., "Model Checking Embedded Software of an Industrial Knitting Machine", International journal of information technology, communications and convergence, vol. 1, iss. 2, pp. 186-205, 2010

Model Checking Embedded Software of an Industrial Knitting Machine

Bibtex entry :

@article {  RHS+10,
	author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
		and Brauer, J{\"o}rg and Scheuer, Florian },
	title = { Model Checking Embedded Software of an Industrial Knitting
		Machine },
	journal = { International journal of information technology,
		communications and convergence },
	publisher = { Inderscience Publishers },
	pages = { 186-205 },
	volume = { 1 },
	number = { 2 },
	year = { 2010 },
	address = { Genève },
	issn = { 2042-3217 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-064544 },
	cin = { 122810 / 120000 },
	url = { http://inderscience.metapress.com/content/y664g84625r780l0/fulltext.pdf },
}
[BHS09]
Brauer, J., Huuck, R., and Schlich, B., "Interprocedural pointer analysis in Goanna", Electronic notes in theoretical computer science : ENTCS, vol. 254, pp. 65-83, 2009

Interprocedural pointer analysis in Goanna

Bibtex entry :

@article {  BHS09,
	author = { Brauer, J{\"o}rg and Huuck, Ralf and Schlich, Bastian },
	title = { Interprocedural pointer analysis in Goanna },
	journal = { Electronic notes in theoretical computer science : ENTCS },
	publisher = { Elsevier Science },
	pages = { 65-83 },
	volume = { 254 },
	year = { 2009 },
	address = { Amsterdam [u.a.] },
	issn = { 1571-0661 },
	doi = { 10.1016/j.entcs.2009.09.060 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-013641 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/132532 },
}
[BSR+09]
Brauer, J., Schlich, B., Reinbacher, T., and Kowalewski, S., "Stack bounds analysis of microcontroller assembly code", in Proc. Embedded Systems Week 2009 : CODES+ISSS’09, CASES’09, EMSOFT’09 ; Proceedings of the 2009 international conference on Compilers, architecture, and synthesis for embedded systems ; 2009, Grenoble, France, October 11 - 16, 2009, New York, NY, 2009, ACM Press.

Stack bounds analysis of microcontroller assembly code

Bibtex entry :

@inproceedings {  BSR+09,
	author = { Brauer, J{\"o}rg and Schlich, Bastian and Reinbacher, Thomas
		and Kowalewski, Stefan },
	title = { Stack bounds analysis of microcontroller assembly code },
	booktitle = { Embedded Systems Week 2009 : CODES+ISSS’09, CASES’09,
		EMSOFT’09 ; Proceedings of the 2009 international
		conference on Compilers, architecture, and synthesis for
		embedded systems ; 2009, Grenoble, France, October 11 - 16,
		2009 },
	publisher = { ACM Press },
	year = { 2009 },
	address = { New York, NY },
	doi = { 10.1145/1631716.1631721 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-173253 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/100433 },
}
[RBH+09]
Reinbacher, T., Brauer, J., Horauer, M., and Schlich, B., "Refining assembly code static analysis for the Intel MCS-51 microcontroller", in Proc. 2009 IEEE International Symposium on Industrial Embedded Systems (SIES 2009) : Lausanne, Switzerland, 08 - 10 July 2009 / [sponsored by: IEEE Industrial Electronics Society (IES)]), Piscataway, NJ, 2009, IEEE, pp. 161-170.

Refining assembly code static analysis for the Intel MCS-51 microcontroller

Bibtex entry :

@inproceedings {  RBH+09,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Schlich, Bastian },
	title = { Refining assembly code static analysis for the Intel MCS-51
		microcontroller },
	booktitle = { 2009 IEEE International Symposium on Industrial Embedded
		Systems (SIES 2009) : Lausanne, Switzerland, 08 - 10 July
		2009 / [sponsored by: IEEE Industrial Electronics Society
		(IES)]) },
	publisher = { IEEE },
	pages = { 161-170 },
	year = { 2009 },
	address = { Piscataway, NJ },
	doi = { 10.1109/SIES.2009.5196212 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-172391 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/99425 },
}
[RHS+09]
Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., and Scheuer, F., "Model checking assembly code of an industrial knitting machine", in Proc. Proceedings of the 2009 Fourth International Conference on Embedded and Multimedia Computing : EM-Com 2009 : [December 10-12, 2009, Jeju Island, Korea], Piscataway, NJ, 2009, IEEE, p. 8.

Model checking assembly code of an industrial knitting machine

Bibtex entry :

@inproceedings {  RHS+09,
	author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
		and Brauer, J{\"o}rg and Scheuer, Florian },
	title = { Model checking assembly code of an industrial knitting
		machine },
	booktitle = { Proceedings of the 2009 Fourth International Conference on
		Embedded and Multimedia Computing : EM-Com 2009 : [December
		10-12, 2009, Jeju Island, Korea] },
	publisher = { IEEE },
	pages = { 8 S. },
	year = { 2009 },
	address = { Piscataway, NJ },
	doi = { 10.1109/EM-COM.2009.5402986 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-199048 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/129021 },
}
[SBW+09]
Schlich, B., Brauer, J., Wernerus, J., and Kowalewski, S., "Direct Model Checking of PLC Programs in IL", in Proc. Dependable Control of Discrete Systems (DCDS'09), Bari, Italy, 2009, pp. 28-33.

Direct Model Checking of {PLC} Programs in {IL}

Bibtex entry :

@inproceedings {  SBW+09,
	author = { Schlich, Bastian and Brauer, J{\"o}rg and Wernerus, J{\"o}rg
		and Kowalewski, Stefan },
	title = { Direct Model Checking of {PLC} Programs in {IL} },
	booktitle = { Dependable Control of Discrete Systems (DCDS'09), Bari,
		Italy },
	pages = { 28-33 },
	year = { 2009 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-236337 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752318 },
}
[HFS+08]
PDFBIB
Huuck, R., Fehnker, A., Seefried, S., and Brauer, J., "Goanna: syntactic software model checking"Berlin [u.a.]: Springer, 2008, vol. 5311, pp. 216-221.

Goanna: syntactic software model checking

Bibtex entry :

@inbook {  HFS+08,
	author = { Huuck, Ralf and Fehnker, Ansgar and Seefried, Sean and
		Brauer, J{\"o}rg },
	title = { Goanna: syntactic software model checking },
	booktitle = { Automated technology for verification and analysis : 6th
		international symposium, ATVA 2008, Seoul, Korea, October 20
		- 23, 2008 ; proceedings / Sungdeok (Steve) Cha; Jin-Young
		Choi; Moonzoo Kim; Insup Lee; Mahesh Viswanathan (eds.) },
	publisher = { Springer },
	pages = { 216-221 },
	volume = { 5311 },
	series = { Lecture notes in computer science },
	year = { 2008 },
	address = { Berlin [u.a.] },
	organization = { 6th International Symposium on Automated Technology for
		Verification and Analysis, Seoul (South Korea), 2008-10-20 -
		2008-10-23 },
	doi = { 10.1007/978-3-540-88387-6_17 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-095469 },
}

Invited Talks

  • Existential Quantification as Incremental SAT. Technical University of Denmark, Copenhagen. 10-06-2011.
  • Automatic Abstraction for Binary Code Verification. Aalborg University, Denmark. 13-04-2011.
  • Automatic Abstraction for Intervals using Boolean Formula. Technical University of Munich, Germany. 14-05-2010.
  • Static Analysis in [mc]square. University of Applied Sciences FH Technikum Vienna, Austria. 31-03-2009.

Teaching


RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany