Dr. rer. nat. Sebastian Biallas

Über mich

Ich bin nach Berlin gezogen.

Am Lehrstuhl habe ich das DFG Projekt „Verifikation von SPS-Programmen mittels Model-Checking und statischer Analyse“ bearbeitet. Speicherprogrammierbare Steuerungen (SPSen) sind Steuerungscomputer zur Automatisierung, Regelung und Steuerung von großtechnischen Anlagen und Maschinen. In diesem Projekt geht es darum, mittels formaler Methoden Fehler in SPS-Programmen zu finden oder zu beweisen, dass sie ihre Spezifikation erfüllen. Insbesondere ist es dazu nötig, geeignete Abstraktion-Techniken zu entwickeln, die es erlauben, Berechnungsschritte auf einer großen Menge von Werten gleichzeitig auszuführen. Erst so ist es möglich, die Analysen auf größere SPS-Programme anzuwenden.

Ich bin weiterhin unter biallas[at]embedded[dot]rwth-aachen[dot]de erreichbar.

Publikationen


Publikations-Export
[Bia16]
Biallas, S., "Verification of programmable logic controller code using model checking and static analysis", PhD Thesis, Aachen, 2016.

Verification of programmable logic controller code using model checking and static analysis

Bibtex entry :

@phdthesis {  Bia16,
	author = { Biallas, Sebastian },
	othercontributors = { Kowalewski, Stefan and Fay, Alexander },
	title = { Verification of programmable logic controller code using
		model checking and static analysis },
	publisher = { Shaker Verlag },
	school = { RWTH Aachen University },
	pages = { 1 Online-Ressource (x, 153 Seiten) : Illustrationen,
		Diagramme },
	series = { Aachener Informatik Berichte },
	year = { 2016 },
	address = { Aachen },
	isbn = { 978-3-8440-4711-0 },
	typ = { PUB:(DE-HGF)29 },
	reportid = { RWTH-2016-06614 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/668156/files/668156.pdf },
}
[BFS+15]
Biallas, S., Friedrich, N., Simon, H., and Kowalewski, S., "Automatic Error Cause Localization of Faulty PLC Programs", IFAC-PapersOnLine, vol. 48, iss. 7, pp. 79-84, 2015

Automatic Error Cause Localization of Faulty PLC Programs

Bibtex entry :

@article {  BFS+15,
	author = { Biallas, Sebastian and Friedrich, Nico and Simon, Hendrik
		and Kowalewski, Stefan },
	title = { Automatic Error Cause Localization of Faulty PLC Programs },
	journal = { IFAC-PapersOnLine },
	publisher = { IFAC },
	pages = { 79-84 },
	volume = { 48 },
	number = { 7 },
	year = { 2015 },
	address = { Laxenburg },
	issn = { 2405-8963 },
	organization = { 5th IFAC International Workshop on Dependable Control of
		Discrete Systems, Cancun (Mexico), 2015-05-27 - 2015-05-29 },
	doi = { 10.1016/j.ifacol.2015.06.476 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-2016-03746 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/573801 },
}
[BSK+15]
Biallas, S., Simon, H., Kowalewski, S., Hauck-Stattelmann, S., and Schlich, B., "Automatische Testfallgenerierung für SPS-Programme mittels Zeilenüberdeckung"Düsseldorf: VDI, 2015, vol. 2258,2, pp. 95-106.

Automatische Testfallgenerierung für SPS-Programme mittels Zeilenüberdeckung

Bibtex entry :

@inbook {  BSK+15,
	author = { Biallas, Sebastian and Simon, Hendrik and Kowalewski, Stefan
		and Hauck-Stattelmann, Stefan and Schlich, Bastian },
	title = { Automatische Testfallgenerierung f{\"u}r SPS-Programme
		mittels Zeilen{\"u}berdeckung },
	booktitle = { Automation 2015 : benefits of change - the future of
		automation ; 16. Branchentreff der Mess- und
		Automatisierungstechnik ; Kongresshaus Baden-Baden, 11. und
		12. Juni 2015 / VDI/VDE-Gesellschaft Mess- und
		Automatisierungstechnik. - Bd. 1 },
	publisher = { VDI },
	pages = { 95-106 },
	volume = { 2258,2 },
	series = { VDI-Berichte },
	year = { 2015 },
	address = { D{\"u}sseldorf },
	organization = { 16. Branchentreff der Mess-und Automatisierungstechnik
		Automation 2015, Baden-Baden (Germany), 2015-06-11 -
		2015-06-12 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-207912 },
	cin = { 122810 / 120000 },
	url = { http://publications.embedded.rwth-aachen.de/file/5r },
}
[HBS+15]
Hauck-Stattelmann, S., Biallas, S., Schlich, B., Kowalewski, S., and Jetley, R., "Analyzing the Restart Behavior of Industrial Control Applications"Springer International Publishing: Cham, 2015, vol. 9109, pp. 585-588.

Analyzing the Restart Behavior of Industrial Control Applications

Bibtex entry :

@inbook {  HBS+15,
	author = { Hauck-Stattelmann, Stefan and Biallas, Sebastian and
		Schlich, Bastian and Kowalewski, Stefan and Jetley, Raoul },
	title = { Analyzing the Restart Behavior of Industrial Control
		Applications },
	booktitle = { FM 2015: formal methods : 20th international symposium,
		Oslo, Norway, June 24 - 26, 2015 ; proceedings / Nikolaj
		Bjørner; Frank de Boer (eds.) },
	publisher = { Cham },
	pages = { 585-588 },
	volume = { 9109 },
	series = { Lecture Notes in Computer Science },
	year = { 2015 },
	address = { Springer International Publishing },
	organization = { 20th International Symposium Formal Methods, Oslo (Norway),
		2015-06-24 - 2015-06-26 },
	doi = { 10.1007/978-3-319-19249-9_38 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-207691 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/541096 },
}
[SFB+15]
Simon, H., Friedrich, N., Biallas, S., Hauck-Stattelmann, S., Schlich, B., and Kowalewski, S., "Automatic test case generation for PLC programs using coverage metrics", in Proc. 2015 IEEE 20th Conference on Emerging Technologies & Factory Automation (ETFA) : 8 - 11 Sept. 2015, City of Luxembourg, Luxembourg / co-sponsored by IEEE ..., Piscataway, NJ, 2015, IEEE, p. 4.

Automatic test case generation for PLC programs using coverage metrics

Bibtex entry :

@inproceedings {  SFB+15,
	author = { Simon, Hendrik and Friedrich, Nico and Biallas, Sebastian
		and Hauck-Stattelmann, Stefan and Schlich, Bastian and
		Kowalewski, Stefan },
	title = { Automatic test case generation for PLC programs using
		coverage metrics },
	booktitle = { 2015 IEEE 20th Conference on Emerging Technologies & Factory
		Automation (ETFA) : 8 - 11 Sept. 2015, City of Luxembourg,
		Luxembourg / co-sponsored by IEEE ... },
	publisher = { IEEE },
	pages = { 4 S. },
	year = { 2015 },
	address = { Piscataway, NJ },
	organization = { 2015 IEEE 20th Conference on Emerging Technologies & Factory
		Automation, Luxembourg (Luxembourg), 2015-09-08 - 2015-09-11 },
	doi = { 10.1109/ETFA.2015.7301602 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-2015-07849 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/565382 },
}
[BKS+14]
Biallas, S., Kowalewski, S., Stattelmann, S., and Schlich, B., "Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code", in Proc. Discrete Event Systems : [Proc. Proceedings of the 12th International Workshop on Discrete Event Systems, Cachan, France, 2014] / Conference Editor: Lesage, Jean-Jacques, Faure, Jean-Marc, Cury, Jose E. R., Lennartson, Bengt, Cachan, France, 2014, IFAC, pp. 400-405.

Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code

Bibtex entry :

@inproceedings {  BKS+14,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Stattelmann,
		Stefan and Schlich, Bastian },
	title = { Efficient Handling of States in Abstract Interpretation of
		Industrial Programmable Logic Controller Code },
	booktitle = { Discrete Event Systems : [Proc. Proceedings of the 12th
		International Workshop on Discrete Event Systems, Cachan,
		France, 2014] / Conference Editor: Lesage, Jean-Jacques,
		Faure, Jean-Marc, Cury, Jose E. R., Lennartson, Bengt },
	publisher = { IFAC },
	pages = { 400-405 },
	year = { 2014 },
	address = { Cachan, France },
	doi = { 10.3182/20140514-3-FR-4046.00065 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-205968 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/443854 },
}
[SKB+14]
Stattelmann, S., Kowalewski, S., Biallas, S., and Schlich, B., "Applying Static Code Analysis on Industrial Controller Code", in Proc. 2014 IEEE [International Conference on] Emerging Technologies and Factory Automation (ETFA 2014) : Barcelona, Spain, 16 - 19 September 2014 / [co-sponsored by Universitat Politècnica de Catalunya - Barcelona Tech (UPC); IEEE Industrial Electronics Society], Piscataway, NJ, 2014, IEEE, p. 4.

Applying Static Code Analysis on Industrial Controller Code

Bibtex entry :

@inproceedings {  SKB+14,
	author = { Stattelmann, Stefan and Kowalewski, Stefan and Biallas,
		Sebastian and Schlich, Bastian },
	title = { Applying Static Code Analysis on Industrial Controller Code },
	booktitle = { 2014 IEEE [International Conference on] Emerging
		Technologies and Factory Automation (ETFA 2014) : Barcelona,
		Spain, 16 - 19 September 2014 / [co-sponsored by Universitat
		Politècnica de Catalunya - Barcelona Tech (UPC); IEEE
		Industrial Electronics Society] },
	publisher = { IEEE },
	pages = { 4 Seiten },
	year = { 2014 },
	address = { Piscataway, NJ },
	organization = { 2014 IEEE [International Conference on] Emerging
		Technologies and Factory Automation, Barcelona (Spain),
		2014-09-16 - 2014-09-19 },
	doi = { 10.1109/ETFA.2014.7005254 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-206434 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/444619 },
}
[BBK13]
Biallas, S., Bohlender, D., and Kowalewski, S., "Boolean and Modular Abstractions for Programmable Logic Controllers", in Proc. Dependable Control of Discrete Systems : DCDS13. - Vol. 4, P. 1, Laxenburg, 2013, IFAC, pp. 97-102.

Boolean and Modular Abstractions for Programmable Logic Controllers

Bibtex entry :

@inproceedings {  BBK13,
	author = { Biallas, Sebastian and Bohlender, Dimitri and Kowalewski,
		Stefan },
	title = { Boolean and Modular Abstractions for Programmable Logic
		Controllers },
	booktitle = { Dependable Control of Discrete Systems : DCDS13. - Vol. 4,
		P. 1 },
	publisher = { IFAC },
	pages = { 97-102 },
	year = { 2013 },
	address = { Laxenburg },
	doi = { 10.3182/20130904-3-UK-4041.00011 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-203363 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/225788 },
}
[BGK13]
Biallas, S., Giacobbe, M., and Kowalewski, S., "Predicate Abstraction for Programmable Logic Controllers"Berlin, Heidelberg ; s.l.: Springer Berlin Heidelberg ; Imprint: Springer, 2013, vol. 8187, pp. 123-138.

Predicate Abstraction for Programmable Logic Controllers

Bibtex entry :

@inbook {  BGK13,
	author = { Biallas, Sebastian and Giacobbe, Mirco and Kowalewski,
		Stefan },
	title = { Predicate Abstraction for Programmable Logic Controllers },
	booktitle = { Formal Methods for Industrial Critical Systems : 18th
		International Workshop, FMICS 2013, Madrid, Spain, September
		23-24, 2013. Proceedings / edited by Charles Pecheur,
		Michael Dierkes },
	publisher = { Springer Berlin Heidelberg ; Imprint: Springer },
	pages = { 123-138 },
	volume = { 8187 },
	series = { Lecture notes in computer science },
	year = { 2013 },
	address = { Berlin, Heidelberg ; s.l. },
	doi = { 10.1007/978-3-642-41010-9_9 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-203367 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/225793 },
}
[BKK+13]
Biallas, S., Kamin, V., Kowalewski, S., Schlich, B., Sehestedt, S., and Stattelmann, S., "Verifikation von sicherheitsgerichteten SPS-Programmen mit Hilfe von Safety-Automaten"Düsseldorf: VDI-Verl., 2013, vol. 2209, pp. 75-79.

Verifikation von sicherheitsgerichteten SPS-Programmen mit Hilfe von Safety-Automaten

Bibtex entry :

@inbook {  BKK+13,
	author = { Biallas, Sebastian and Kamin, Volker and Kowalewski, Stefan
		and Schlich, Bastian and Sehestedt, Stephan and Stattelmann,
		Stefan },
	title = { Verifikation von sicherheitsgerichteten SPS-Programmen mit
		Hilfe von Safety-Automaten },
	booktitle = { Automation 2013 : 14. Branchentreff der Mess- und
		Automatisierungstechnik ; Kongresshaus Baden-Baden, 25. und
		26. Juni 2013 / VDI/VDE-Gesellschaft Mess- und
		Automatisierungstechnik },
	publisher = { VDI-Verl. },
	pages = { 75-79 },
	volume = { 2209 },
	series = { VDI-Berichte },
	year = { 2013 },
	address = { D{\"u}sseldorf },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-203699 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/226206 },
}
[BMC+13]
Biallas, S., Mads, C. O., Cassez, F., and Huuck, R., "PtrTracker: Pragmatic pointer analysis", in Proc. 2013 IEEE 13th International Working Conference on Source Code Analysis and Manipulation (SCAM) : 22 - 23 Sept. 2013, Eindhoven, the Netherlands / sponsors: IEEE Computer Society Technical Council on Software Engineering ... Ed.: Bram Adams ..., Piscataway, NJ, 2013, IEEE, pp. 69-73.

PtrTracker: Pragmatic pointer analysis

Bibtex entry :

@inproceedings {  BMC+13,
	author = { Biallas, Sebastian and Mads, Chr. Olesen and Cassez, Franck
		and Huuck, Ralf },
	title = { PtrTracker: Pragmatic pointer analysis },
	booktitle = { 2013 IEEE 13th International Working Conference on Source
		Code Analysis and Manipulation (SCAM) : 22 - 23 Sept. 2013,
		Eindhoven, the Netherlands / sponsors: IEEE Computer Society
		Technical Council on Software Engineering ... Ed.: Bram
		Adams ... },
	publisher = { IEEE },
	pages = { 69-73 },
	year = { 2013 },
	address = { Piscataway, NJ },
	organization = { 2013 IEEE 13th International Working Conference on Source
		Code Analysis and Manipulation, Eindhoven (Netherlands),
		2013-09-22 - 2013-09-23 },
	doi = { 10.1109/SCAM.2013.6648186 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-236321 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752296 },
}
[BBK+12]
Biallas, S., Brauer, J., King, A., and Kowalewski, S., "Loop Leaping with Closures", in Proc. Static Analysis : 19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012. Proceedings / edited by Antoine Miné, David Schmidt, Berlin, Heidelberg, 2012 in Lecture Notes in Computer Science, Springer, 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 = { 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 },
}
[BBK12]
Beckschulze, E., Biallas, S., and Kowalewski, S., "Static Analysis of Lockless Microcontroller C Programs", in Proc. Proceedings Seventh Conference on Systems Software Verification (SSV 2012) : Sydney, Australia, 28-30 November 2012 / Franck Cassez, Ralf Huuck, Gerwin Klein and Bastian Schlich, Sydney, Australia, 2012 in Electronic proceedings in theoretical computer science : EPTCS, pp. 103-114.

Static Analysis of Lockless Microcontroller C Programs

Bibtex entry :

@inproceedings {  BBK12,
	author = { Beckschulze, Eva and Biallas, Sebastian and Kowalewski,
		Stefan },
	title = { Static Analysis of Lockless Microcontroller C Programs },
	booktitle = { Proceedings Seventh Conference on Systems Software
		Verification (SSV 2012) : Sydney, Australia, 28-30 November
		2012 / Franck Cassez, Ralf Huuck, Gerwin Klein and Bastian
		Schlich },
	pages = { 103-114 },
	series = { Electronic proceedings in theoretical computer science :
		EPTCS },
	year = { 2012 },
	address = { Sydney, Australia },
	doi = { 10.4204/EPTCS.102.10 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-195461 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/124829 },
}
[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 },
}
[BKS12]
Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse von SPS-Programmen", in Proc. Automation 2012 : der 13. Branchentreff der Mess- und Automatisierungstechnik / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik ; Kongress 'Automation 2012' ; 13 (Baden-Baden) ; 2011.06.13-14Branchentreff der Mess- und Automatisierungstechnik, Düsseldorf, 2012 in VDI-Berichte, VDI-Verl., pp. 79-83.

Automatische Wertebereichsanalyse von SPS-Programmen

Bibtex entry :

@inproceedings {  BKS12,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Automatische Wertebereichsanalyse von SPS-Programmen },
	booktitle = { Automation 2012 : der 13. Branchentreff der Mess- und
		Automatisierungstechnik / VDI/VDE-Gesellschaft Mess- und
		Automatisierungstechnik ; Kongress 'Automation 2012' ; 13
		(Baden-Baden) ; 2011.06.13-14Branchentreff der Mess- und
		Automatisierungstechnik },
	publisher = { VDI-Verl. },
	pages = { 79-83 },
	series = { VDI-Berichte },
	year = { 2012 },
	address = { D{\"u}sseldorf },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-191631 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/120638 },
}
[BKS12a]
Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme", Automatisierungstechnische Praxis : atp, vol. 54, iss. 7/8, pp. 68-74, 2012

Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme

Bibtex entry :

@article {  BKS12a,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Automatische Wertebereichsanalyse -- Formale Verifikation
		f{\"u}r SPS-Programme },
	journal = { Automatisierungstechnische Praxis : atp },
	publisher = { Oldenbourg Industrieverl. },
	pages = { 68-74 },
	volume = { 54 },
	number = { 7/8 },
	year = { 2012 },
	address = { M{\"u}nchen },
	issn = { 0178-2320 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-015025 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/133988 },
}
[BKS12b]
Biallas, S., Kowalewski, S., and Schlich, B., "Range and Value-Set Analysis for Programmable Logic Controllers", in Proc. Proceedings of the 11th International Workshop on Discrete Event Systems, Guadalajara, Mexico, 2012, IFAC, pp. 378-383.

Range and Value-Set Analysis for Programmable Logic Controllers

Bibtex entry :

@inproceedings {  BKS12b,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Range and Value-Set Analysis for Programmable Logic
		Controllers },
	booktitle = { Proceedings of the 11th International Workshop on Discrete
		Event Systems },
	publisher = { IFAC },
	pages = { 378-383 },
	year = { 2012 },
	address = { Guadalajara, Mexico },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-236327 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752302 },
}
[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 },
}
[BKS11]
Biallas, S., Kowalewski, S., and Schlich, B., "Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse", in Proc. 'Zukunft verantwortungsvoll gestalten' : Automation 2011 ; der 12. Branchentreff der Mess- und Automatisierungstechnik ; Kongress Baden-Baden, 28. und 29. Juni 2011 / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik. [Kongressleiter: Peter Adolphs ...], Düsseldorf, 2011 in VDI-Berichte, VDI-Verl., pp. 67-72.

Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse

Bibtex entry :

@inproceedings {  BKS11,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Leistungsf{\"a}hige Verifikation von industriellen
		SPS-Programmen mittels Model-Checking und statischer Analyse },
	booktitle = { 'Zukunft verantwortungsvoll gestalten' : Automation 2011 ;
		der 12. Branchentreff der Mess- und Automatisierungstechnik
		; Kongress Baden-Baden, 28. und 29. Juni 2011 /
		VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik.
		[Kongressleiter: Peter Adolphs ...] },
	publisher = { VDI-Verl. },
	pages = { 67-72 },
	series = { VDI-Berichte },
	year = { 2011 },
	address = { D{\"u}sseldorf },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-189475 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/118212 },
}
[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 },
}
[BFK+10]
Biallas, S., Frey, G., Kowalewski, S., Schlich, B., and Soliman, D., "Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene", in Proc. Entwurf komplexer Automatisierungssysteme : EKA 2010 ; Beschreibungsmittel, Methoden, Werkzeuge und Anwendungen ; 11. Fachtagung mit Tutorium, 25. bis 27. Mai 2010 in Magdeburg, Denkfabrik im Wissenschaftshafen / ifak, Institut für Automation und Kommunikation e.V., Magdeburg; Otto-von-Guericke-Universität Magdeburg, Institut für Automatisierungstechnik. [Hrsg.: Ulrich Jumar, Eckehard Schnieder, Christian Diedrich], Magdeburg, 2010, ifak, pp. 49-57.

Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene

Bibtex entry :

@inproceedings {  BFK+10,
	author = { Biallas, Sebastian and Frey, Georg and Kowalewski, Stefan
		and Schlich, Bastian and Soliman, Doaa },
	title = { Formale Verifikation von Sicherheits-Funktionsbausteinen der
		PLCopen auf Modell- und Code-Ebene },
	booktitle = { Entwurf komplexer Automatisierungssysteme : EKA 2010 ;
		Beschreibungsmittel, Methoden, Werkzeuge und Anwendungen ;
		11. Fachtagung mit Tutorium, 25. bis 27. Mai 2010 in
		Magdeburg, Denkfabrik im Wissenschaftshafen / ifak, Institut
		f{\"u}r Automation und Kommunikation e.V., Magdeburg;
		Otto-von-Guericke-Universit{\"a}t Magdeburg, Institut
		f{\"u}r Automatisierungstechnik. [Hrsg.: Ulrich Jumar,
		Eckehard Schnieder, Christian Diedrich] },
	publisher = { ifak },
	pages = { 49-57 },
	year = { 2010 },
	address = { Magdeburg },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190099 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/118924 },
}

RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland