Wed 11 May 2022 20:15 - 20:20 at ICSE room 3-even hours - Validation and Verification 5 Chair(s): Saba Alimadadi
Wed 25 May 2022 11:15 - 11:20 at Ballroom A - Papers 5: Validation and Verification Chair(s): Shiva Nejati
Neural networks can be regarded as a new programming paradigm, i.e., instead of building ever-more complex programs through (often informal) logical reasoning in the programmers’ mind, complex `AI’ systems are built by optimising generic neural network models with big data. In this new paradigm, AI frameworks such as TensorFlow and PyTorch play a key role, which is as essential as the compiler for traditional programs. It is known that the lack of a proper semantics for programming languages (such as C), i.e., a correctness specification for compilers, has contributed to many problematic program behaviours and security issues. While it is in general hard to have a correctness specification for compilers due to the high complexity of programming languages and their rapid evolution, we have a unique opportunity to do it right this time for neural networks (which have a limited set of functions, and most of them have stable semantics). In this work, we report our effort on providing a correctness specification of neural network frameworks such as TensorFlow. We specify the semantics of almost all TensorFlow layers in the logical programming language Prolog. We demonstrate the usefulness of the semantics through two applications. One is a fuzzing engine for TensorFlow, which features a strong oracle and a systematic way of generating valid neural networks. The other is a model validation approach which enables consistent bug reporting for TensorFlow models.
Tue 10 MayDisplayed time zone: Eastern Time (US & Canada) change
Wed 11 MayDisplayed time zone: Eastern Time (US & Canada) change
Wed 25 MayDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30 | Papers 5: Validation and VerificationSEIP - Software Engineering in Practice / Technical Track / Journal-First Papers at Ballroom A Chair(s): Shiva Nejati University of Ottawa | ||
11:00 5mTalk | Linear-time Temporal Logic guided Greybox Fuzzing Technical Track Ruijie Meng National University of Singapore, Singapore, Zhen Dong Fudan University, China, Jialin Li National University of Singapore, Singapore, Ivan Beschastnikh University of British Columbia, Abhik Roychoudhury National University of Singapore DOI Pre-print Media Attached | ||
11:05 5mTalk | Verification of Consistency between Process Models, Object Life Cycles, and Context-dependent Semantic Specifications Journal-First Papers Ralph Hoch Institute of Computer Technology, TU Wien, Christoph Luckeneder Vienna University of Technology, Roman Popp TU Wien, Vienna, Austria, Hermann Kaindl Institute of Computer Technology, TU Wien Link to publication DOI Pre-print Media Attached | ||
11:10 5mTalk | GraphFuzz: Library API Fuzzing with Lifetime-aware Dataflow Graphs Technical Track DOI Pre-print Media Attached | ||
11:15 5mTalk | ExAIS: Executable AI Semantics Technical Track Pre-print Media Attached | ||
11:20 5mTalk | Verifying Dynamic Trait Objects in Rust SEIP - Software Engineering in Practice Alexa VanHattum Cornell University, Daniel Schwartz-Narbonne Amazon, n.n., Nathan Chong Amazon, Adrian Sampson Cornell University Pre-print Media Attached | ||
11:25 5mTalk | Quantifying Permissiveness of Access Control Policies Technical Track William Eiers University of California at Santa Barbara, USA, Ganesh Sankaran University of California Santa Barbara, Albert Li University of California Santa Barbara, Emily O'Mahony University of California Santa Barbara, Benjamin Prince University of California Santa Barbara, Tevfik Bultan University of California, Santa Barbara Pre-print Media Attached | ||
11:30 5mTalk | Fuzzing Class Specifications Technical Track Facundo Molina University of Rio Cuarto and CONICET, Argentina, Marcelo d'Amorim Federal University of Pernambuco, Nazareno Aguirre University of Rio Cuarto and CONICET, Argentina Pre-print Media Attached | ||