Peer-reviewed research, books, and technical work from the Assurance Labs team on software correctness, formal methods, and high-assurance engineering.
Richard C. Linger
AIAA ASCEND 2026, Washington, DC
Computing the behavior of aerospace software to verify functionality, correctness and cybersecurity, presented at AIAA ASCEND 2026.
Read publicationRichard C. Linger, John McHugh, Ali Mili, Mark G. Pleszkoch, Wided Ghardallou, Jack McGaughey
AIAA Aviation Forum and ASCEND 2024, Las Vegas, NV
Argues for correctness and security verification of the software running off-world systems. AIAA 2024-4850.
Read publicationRichard C. Linger, Mark G. Pleszkoch, Jack McGaughey, John McHugh, Wided Ghardallou, Ali Mili
New Security Paradigms Workshop (NSPW)
Function extraction as a new paradigm for producing secure code, presented at the New Security Paradigms Workshop.
Read publicationWided Ghardallou, Hessamaldin Mohammadi, Richard C. Linger, Mark G. Pleszkoch, Ji Meng Loh, Ali Mili
Acta Informatica 61(3)
Derives invariant relations for affine loops, giving a relational basis for computing the function of loop code.
Read publicationRichard C. Linger, Ali Mili, Robert Drazovich, Mark G. Pleszkoch, John McHugh, Wided Ghardallou
AIAA 2023-2471
Case for provably correct software in space systems. AIAA 2023-2471, Computer Systems session.
Read publicationHessamaldin Mohammadi, Wided Ghardallou, Richard C. Linger, Ali Mili
FormaliSE @ ICSE (International Conference on Formal Methods in Software Engineering)
Computes program functions from source code, extending function extraction to produce exact behavioral specifications.
Read publicationHessamaldin Mohammadi, Wided Ghardallou, Ali Mili
IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C)
Presents assume, capture, verify and establish as ingredients for scalable software analysis.
Read publicationRichard C. Linger
70th International Astronautical Congress (IAC 2019), Washington, DC
Behavior computation as a knowledge management process for validating the cybersecurity of aerospace software. Paper IAC-19,D5,4,5,x49838.
Read publicationRichard C. Linger
AIAA SPACE and Astronautics Forum and Exposition 2018, Orlando, FL
Behavior computation of aerospace software for validating security and functionality. AIAA 2018-5274.
Read publicationNafi Diallo, Wided Ghardallou, Jules Desharnais, Ali Mili
Journal of Logical and Algebraic Methods in Programming 97
Unifies termination and abort-freedom into a single convergence property and shows how it can be verified.
Read publicationMark G. Pleszkoch, Richard C. Linger
Cyber and Information Security Research Conference (CISR)
Controls the combinatorial complexity of path explosion so that software and malware behavior can be computed in practice.
Read publicationOlfa Mraihi, Asma Louhichi, Lamia Labed Jilani, Jules Desharnais, Ali Mili
Science of Computer Programming 78(9)
Compares invariant assertions, invariant relations and invariant functions, and shows how each supports loop analysis.
Read publicationRichard C. Linger, Mark G. Pleszkoch, Stacy J. Prowell, Kirk Sayre, T. Scott Ankrum
Cyber Security and Information Intelligence Research Workshop (CSIIRW)
Demonstrates function extraction on an IBM/370 system to compute the behavior of legacy software and expose its functionality and security properties.
Read publicationLamia Labed Jilani, Olfa Mraihi, Asma Louhichi, Wided Ghardallou, Khaled Bsaïes, Ali Mili
Journal of Symbolic Computation 48
Introduces invariant functions and invariant relations as an alternative to invariant assertions for reasoning about loops.
Read publicationLamia Labed Jilani, Asma Louhichi, Olfa Mraihi, Ali Mili
Innovations in Systems and Software Engineering 8(3)
Develops invariant relations, invariant functions and loop functions as complementary techniques for computing what a loop does.
Read publicationStacy J. Prowell, Mark G. Pleszkoch, Kirk Sayre, Richard C. Linger
IEEE PES Innovative Smart Grid Technologies (ISGT)
Automated vulnerability detection applied to compiled smart grid software.
Read publicationMark G. Pleszkoch, Richard C. Linger, Stacy J. Prowell, Kirk Sayre, Luanne Burns
Hawaii International Conference on System Sciences (HICSS)
Applies automated behavior computation to software analysis and validation at system scale.
Read publicationRichard C. Linger, Kirk Sayre, Tim Daly, Mark G. Pleszkoch
Hawaii International Conference on System Sciences (HICSS)
Applies function extraction technology to compute the behavior of malware instead of relying on signatures.
Read publicationRichard C. Linger, Tim Daly, Mark G. Pleszkoch
Software Engineering Institute, Carnegie Mellon University
2010 development and application of semantic reduction theorems for behavior analysis. Software Engineering Institute technical report, February 2011.
Read publicationRichard C. Linger, Mark G. Pleszkoch, Stacy J. Prowell, Kirk Sayre
Cyber Security and Information Intelligence Research Workshop (CSIIRW)
Behavior computation applied to smart grid software analysis.
Read publicationAli Mili, Shir Aharon, Chaitanya Nadkarni
Science of Computer Programming 74(11-12)
Develops the mathematics for reasoning about the functions computed by loops, including nested and non-linear cases.
Read publicationMark G. Pleszkoch, Richard C. Linger, Alan R. Hevner
The DATA BASE for Advances in Information Systems 39(3)
Introduces function extraction into software testing by computing program behavior for verification.
Read publication