Automata Learning for Symbolic Execution

Bernhard Aichernig; Roderick Bloem; Masoud Ebrahimi; Martin Tappler; Johannes Winter

Automata Learning for Symbolic Execution

Bernhard Aichernig
, Roderick Bloem
, Masoud Ebrahimi
, Martin Tappler
, Johannes Winter

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Abstract

Black-box components conceal parts of software execution paths, which makes systematic testing, e. g., via symbolic execution, difficult. In this paper, we use automata learning to facilitate symbolic execution in the presence of black-box components. We substitute black boxes in a software system with learned automata that model them, enabling us to symbolically execute program paths that run through black-boxes. We show that applying the approach on real-world software systems incorporating black-boxes increases code coverage when compared to standard techniques.

Original language	English
Title of host publication	2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018
Editors	Nikolaj Bjørner, Arie Gurfinkel
Publisher	IEEE CS
Pages	130 - 138
Number of pages	9
ISBN (Electronic)	978-0-9835678-8-2
Publication status	Published - 2018
Event	18th Conference on Formal Methods in Computer-Aided Design - Austin, United States Duration: 30 Oct 2018 → 2 Nov 2018 Conference number: 18

Conference

Conference	18th Conference on Formal Methods in Computer-Aided Design
Abbreviated title	FMCAD 2018
Country/Territory	United States
City	Austin
Period	30/10/18 → 2/11/18

Access to Document

https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/fmcad2018_proceedings.pdf

Enable-S3 - European Initiative to Enable Validation for Highly Automated Safe and Secure Systems
Eichberger, A. (Project manager on research unit), Bloem, R. (Project manager on research unit), Wotawa, F. (Project manager on research unit), Horn, M. (Project manager on research unit), Bösch, W. (Consortium manager resp. coordinator of internal research units) & Bösch, W. (Project manager on research unit)
1/05/16 → 30/04/19
Project: Research project
Dependable Internet of Things
Pernkopf, F. (Contact person), Zakany, N. (Contact person), Eichlseder, M. (Contact person), Saukh, O. (Contact person), Mangard, S. (Contact person), Steinbauer-Wagner, G. (Contact person), Knoll, C. (Attendee / Assistant), Tranninger, M. (Attendee / Assistant), Römer, K. U. (Consortium manager resp. coordinator of internal research units), Rath, M. (Attendee / Assistant), Kubin, G. (Contact person), Horn, M. (Contact person), Tappler, M. (Attendee / Assistant), Bloem, R. (Consortium manager resp. coordinator of internal research units), Weiser, S. (Attendee / Assistant), Leitinger, E. (Contact person), Ebrahimi, M. (Attendee / Assistant), Aichernig, B. (Contact person), Malenko, M. (Attendee / Assistant), Steinberger, M. (Contact person), Großwindhager, B. (Attendee / Assistant), Baunach, M. C. (Contact person), Witrisal, K. (Contact person), Teschl, R. (Contact person), Boano, C. A. (Contact person), Alothman Alterkawi, A. B. (Attendee / Assistant), Bösch, W. (Contact person) & Grosinger, J. (Contact person)
1/01/16 → 31/03/22
Project: Research project
EU - IMMORTAL - IMMORTAL – Integrated Modelling, Fault Management, Verification and Reliable Design Environment for Cyber-Physical Systems
Könighofer, R. (Attendee / Assistant) & Bloem, R. (Project manager on research unit)
1/03/15 → 28/02/18
Project: Research project

Cite this

Automata Learning for Symbolic Execution. / Aichernig, Bernhard ; Bloem, Roderick; Ebrahimi, Masoud et al.
2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. ed. / Nikolaj Bjørner; Arie Gurfinkel. IEEE CS, 2018. p. 130 - 138.

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Aichernig, B , Bloem, R, Ebrahimi, M, Tappler, M & Winter, J 2018, Automata Learning for Symbolic Execution. in N Bjørner & A Gurfinkel (eds), 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. IEEE CS, pp. 130 - 138, 18th Conference on Formal Methods in Computer-Aided Design, Austin, Texas, United States, 30/10/18. <https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/fmcad2018_proceedings.pdf>

@inproceedings{1a2e8f78853e4a5ca71a3e0ec0c2c415,

title = "Automata Learning for Symbolic Execution",

abstract = "Black-box components conceal parts of software execution paths, which makes systematic testing, e. g., via symbolic execution, difficult. In this paper, we use automata learning to facilitate symbolic execution in the presence of black-box components. We substitute black boxes in a software system with learned automata that model them, enabling us to symbolically execute program paths that run through black-boxes. We show that applying the approach on real-world software systems incorporating black-boxes increases code coverage when compared to standard techniques.",

author = "Bernhard Aichernig and Roderick Bloem and Masoud Ebrahimi and Martin Tappler and Johannes Winter",

year = "2018",

language = "English",

pages = "130 -- 138",

editor = "Bj{\o}rner, \{Nikolaj \} and Gurfinkel, \{Arie \}",

booktitle = "2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018",

publisher = "IEEE CS",

note = "18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018 ; Conference date: 30-10-2018 Through 02-11-2018",

}

TY - GEN

T1 - Automata Learning for Symbolic Execution

AU - Aichernig, Bernhard

AU - Bloem, Roderick

AU - Ebrahimi, Masoud

AU - Tappler, Martin

AU - Winter, Johannes

N1 - Conference code: 18

PY - 2018

Y1 - 2018

N2 - Black-box components conceal parts of software execution paths, which makes systematic testing, e. g., via symbolic execution, difficult. In this paper, we use automata learning to facilitate symbolic execution in the presence of black-box components. We substitute black boxes in a software system with learned automata that model them, enabling us to symbolically execute program paths that run through black-boxes. We show that applying the approach on real-world software systems incorporating black-boxes increases code coverage when compared to standard techniques.

AB - Black-box components conceal parts of software execution paths, which makes systematic testing, e. g., via symbolic execution, difficult. In this paper, we use automata learning to facilitate symbolic execution in the presence of black-box components. We substitute black boxes in a software system with learned automata that model them, enabling us to symbolically execute program paths that run through black-boxes. We show that applying the approach on real-world software systems incorporating black-boxes increases code coverage when compared to standard techniques.

M3 - Conference paper

SP - 130

EP - 138

BT - 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018

A2 - Bjørner, Nikolaj

A2 - Gurfinkel, Arie

PB - IEEE CS

T2 - 18th Conference on Formal Methods in Computer-Aided Design

Y2 - 30 October 2018 through 2 November 2018

ER -

Automata Learning for Symbolic Execution

Abstract

Conference

Access to Document

Fingerprint

Projects

Enable-S3 - European Initiative to Enable Validation for Highly Automated Safe and Secure Systems

Dependable Internet of Things

EU - IMMORTAL - IMMORTAL – Integrated Modelling, Fault Management, Verification and Reliable Design Environment for Cyber-Physical Systems

Cite this