|![]() |
|
Email: brauer[at]embedded[dot]rwth-aachen[dot]de
“Luck favors the prepared mind.“
|
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.
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.
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.
A more detailed list of my publications can be found here (including abstracts), and a list of my co-authors can be found here.
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@article { KPB13, author = { Kowalewski, Stefan 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 : STTT }, publisher = { Springer }, pages = { 287-289 }, volume = { 15 }, number = { 4 }, year = { 2013 }, address = { Berlin ; Heidelberg [u.a.] }, issn = { 1433-2787 }, organization = { 15th International Conference, TACAS 2009, York (UK), 2009-03-22 - 2009-03-29 }, doi = { 10.1007/s10009-013-0280-3 }, typ = { PUB:(DE-HGF)16 }, reportid = { RWTH-CONV-236324 }, cin = { 122810 / 120000 }, url = { http://publications.rwth-aachen.de/record/752289 }, }
@inproceedings { BBK+12, author = { Biallas, Sebastian and Brauer, J{\"o}rg and King, Andy and Kowalewski, Stefan }, title = { Loop Leaping with Closures }, booktitle = { Static Analysis : 19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012. Proceedings / edited by Antoine Miné, David Schmidt }, publisher = { Springer }, pages = { 214-230 }, series = { Lecture Notes in Computer Science }, year = { 2012 }, address = { Berlin, Heidelberg }, organization = { Static Analysis : 19th International Symposium, Deauville (France), 2012-09-11 - 2012-09-13 }, typ = { PUB:(DE-HGF)7 }, reportid = { RWTH-CONV-236335 }, cin = { 122810 / 120000 }, url = { http://publications.rwth-aachen.de/record/752305 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }