| | |
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 }, organization = { Brazilian Symposium on Programming Languages }, 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 }, organization = { Formale Methoden f{\"u}r industriekritische Systeme }, 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 = { 15. 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 : 19. 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 }, organization = { 4. International Workshop on Numerical and Symbolic Abstract Domains (France), 10-09-2012 }, 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 }, organization = { 27. IEEE/ACM International Conference on Automated Software Engineering, Essen (Germany), 2012-09-03 - 2012-09-07 }, 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 }, organization = { 6. International Workshop on Systems Software Verification }, 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.] }, organization = { NASA formal methods : 4. international symposium, Norfolk, VA (USA), 2012-04-03 - 2012-04-05 }, 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 }, organization = { 4. International Workshop on Numerical and Symbolic Abstract Domains (France), 10-09-2010 }, 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.] }, organization = { Formal methods for automation and safety in railway and automotive systems, 2010 }, 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 }, organization = { 3. International Workshop on Dependable Control of Discrete Systems 2011, Saarbr{\"u}cken (Germany), 2011-06-15 - 2011-06-17 }, 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 = { 14. 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.] }, organization = { 3. international symposium: NASA formal methods, Pasadena, CA (USA), 2011-04-18 - 2011-04-20 }, 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.] }, organization = { 20. European Symposium on Programming, Saarbr{\"u}cken (Germany), 2011-03-26 - 2011-04-03 }, 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.] }, organization = { Computer aided verification : 23. international conference, Snowbird, UT (USA), 2011-07-14 - 2011-07-20 }, doi = { 10.1007/978-3-642-22110-1 }, typ = { PUB:(DE-HGF)7 }, 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 }, organization = { 9. ACM international conference on Embedded software, Taipei (Taiwan), 2011-10-09 - 2011-10-14 }, 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.] }, organization = { Formal methods for industrial critical systems : 16. international workshop, Trento (Italy), 2011-08-29 - 2011-08-30 }, 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 }, organization = { Runtime Verification : Second International Conference, San Francisco, CA (USA), 2011-09-27 - 2011-09-30 }, 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 }, organization = { ASME International Design Engineering Technical Conferences and Computers and Information in Engineering Conference - 2011, Washington, DC (USA), 2011-08-28 - 2011-08-31 }, 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.] }, organization = { 5. International Haifa Verification Conference, HCV 2009, Haifa (Israel), 2009-10-19 - 2009-10-22 }, 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 }, organization = { 4. International Workshop on Harnessing Theories for Tool Support in Software, Shanghai (Peoples R China), 2010-11-15 - 2010-11-15 }, typ = { PUB:(DE-HGF)7 }, 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 }, organization = { 5. International Workshop on Systems Software Verification, Vancouver (Canada) }, 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.] }, organization = { Static analysis : 17. international symposium, Perpignan (France), 2010-09-14 - 2010-09-16 }, 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 }, organization = { 5. international conference on Systems software verification }, 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.] }, organization = { Formal methods for industrial critical systems : 15. international workshop, Antwerp (Belgium), 2010-09-20 - 2010-09-21 }, 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 }, organization = { 13. International Workshop on Software & Compilers for Embedded Systems, St. Goar (Germany), 2010-06-29 - 2010-06-30 }, 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 }, organization = { 2010 International Symposium on Industrial Embedded Systems, Trento (Italy), 2010-07-07 - 2010-07-09 }, 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 }, organization = { 13. IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems, Vienna (Austria), 2010-04-14 - 2010-04-16 }, 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 }, organization = { 6. Doctoral Workshop on Mathematical and Engineering Methods in Computer Science }, 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 }, organization = { 2009 international conference on Compilers, architecture, and synthesis for embedded systems, Grenoble (France), 2009-10-11 - 2009-10-16 }, 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 }, organization = { 2009 IEEE International Symposium on Industrial Embedded Systems, Lausanne (Switzerland), 2009-07-08 - 2009-07-10 }, 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 }, organization = { 2009 Fourth International Conference on Embedded and Multimedia Computing, Jeju Island (South Korea), 2009-12-10 - 2009-12-12 }, doi = { 10.1109/EM-COM.2009.5402986 }, typ = { PUB:(DE-HGF)7 }, reportid = { RWTH-CONV-199048 }, cin = { 122810 / 120000 }, url = { http://publications.rwth-aachen.de/record/129021 }, }
@article { 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 }, journal = { IFAC Proceedings Volumes }, publisher = { Elsevier }, pages = { 28-33 }, volume = { 42 }, number = { 5 }, year = { 2009 }, address = { Amsterdam }, issn = { 1474-6670 }, isbn = { 978-3-902661-44-9 }, organization = { 2. IFAC Workshop on Dependable Control of Discrete Systems, Bari (Italy), 2009-06-10 - 2009-06-12 }, doi = { 10.3182/20090610-3-IT-4004.00010 }, typ = { PUB:(DE-HGF)16 }, reportid = { RWTH-CONV-236337 }, cin = { 122810 / 120000 }, url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:SBWK09.pdf }, }
@inproceedings { 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 }, series = { Lecture notes in computer science }, year = { 2008 }, address = { Berlin [u.a.] }, organization = { 6. 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 }, }