NASA Logo, National Aeronautics and Space Administration

+NASA Home

+Ames Home

Dr. Corina Pasareanu Gives an Invited Talk at the Logic in Computer Science (LICS '17) Symposium
Intelligent Systems Division Banner

Dr. Corina Pasareanu Gives an Invited Talk at the Logic in Computer Science (LICS '17) Symposium

Dr. Corina Pasareanu gave an invited talk, entitled “Symbolic Execution and Probabilistic Reasoning” at the 32nd Annual Association for Computing Machinery (ACM) / Institute of Electrical and Electronics Engineers (IEEE) Symposium on Logic in Computer Science (LICS), held on the 20th–23rd of June, 2017, in Reykjavik, Iceland. Symbolic execution is a systematic program analysis technique that explores multiple program behaviors all at once by collecting and solving symbolic path conditions over program paths. The technique has been recently extended with probabilistic reasoning. This approach computes the conditions to reach target program events of interest and uses model counting to quantify the fraction of the input domain satisfying these conditions, thus computing the probability of event occurrence. This probabilistic information can be used, for example, to compute the reliability of an aircraft controller under different wind conditions (modeled probabilistically), or to quantify the leakage of sensitive data in a software system, using information theory metrics such as Shannon entropy. In this talk, Corina reviewed recent advances in symbolic execution and probabilistic reasoning, and discussed how both can be used to ensure the safety and security of software systems.

BACKGROUND: Advanced Verification and Validation (V&V) techniques based on symbolic execution and probabilistic reasoning offer a chance to detect and quantify complex safety and security issues in modern software, even in the presence of changing and unpredictable environments. These new techniques will become increasingly relevant as our aviation systems become more complex and more autonomous. These techniques are at the core of the new research objectives being addressed by the Airspace Operation and Safety Program (AOSP) under the Aeronautics Research and Mission Directorate (ARMD).

POINT OF CONTACT: Corina Pasareanu,

First Gov logo
NASA Logo -