Kosaian and Rozier speak at 2025 Iowa Colloquium on Information, Complexity, and Logic (ICICL)

Laboratory alumna Katherine Kosaian is giving a keynote at the 2025 ICICL! Rozier is giving an invited talk. Registration is free!

https://icicl.wp.drake.edu/conf/

ICICL, the Iowa Colloquium on Information, Complexity, and Logic, a research colloquium run jointly by researchers at Drake University and Iowa State University, will be hosting the third of three NSF-funded summer conferences on June 3-4, 2025.


Katherine Kosaian –  Formalizing mathematics in Isabelle/HOL

Abstract: Many mathematical algorithms are used in safety-critical contexts.  Correctness of these algorithms, and the mathematical results underlying them, is crucial.  In formal methods, a piece of software called a theorem prover can be used to formally verify algorithms. In this approach, code for an algorithm is accompanied by a rigorous proof of correctness that only depends on the logical foundations of the theorem prover.  Algorithms that have been verified in this way are highly trustworthy and thus safe for use in safety-critical applications. 

The theorem prover Isabelle/HOL is well-suited for formalizing mathematics.  This talk will motivate formalized mathematics, exhibit how mathematics is formalized in Isabelle/HOL, and discuss the challenges that may arise, with a focus on three case studies.


Kristin Yvonne Rozier – On the Unusual Effectiveness of Temporal Logic

Abstract: Aside from being a fun and interesting class of modal logic, temporal logics have become essential tools for safety-critical system verification and AI applications including planning and synthesis. We highlight a couple of temporal logics and show some of their real-life, cutting-edge applications. Linear Temporal Logic (LTL) intuitively captures system timelines, and provides a specification language for model checking, the most popular formal verification technique, which exhaustively proves whether a system always upholds its specifications. Mission-time Linear Temporal Logic (MLTL) adds closed-interval integer bounds on the temporal operators of LTL, enabling unit-agnostic specification over finite traces. MLTL optimizes the trade-off between expressibility of a wide range of realistic requirements and the ability to author generic, easy-to-validate formulas that capture concepts commonly seen in, e.g., aerospace operational concepts. We highlight systems where LTL and MLTL requirements play a critical role, including NASA’s Automated Air Traffic Control system, Robonaut2 and the NASA Lunar Gateway Vehicle System Manager.

Leave a Comment

Filed under Lab Alumni, Research Talks

NASA Awards R2U2 Advances for Lunar Gateway Mission

https://www.linkedin.com/embed/feed/update/urn:li:share:7235334577848754176

https://www.linkedin.com/posts/iowa-state-university-department-of-aerospace-engineering_congratulations-to-associate-professor-and-activity-7235334578838609920-ZgSj?utm_source=share&utm_medium=member_desktop

Leave a Comment

Filed under Awards, Laboratory Collaborations

Rozier Gives Invited Talk at AAAI 2023 Spring Symposium Series

On the Effectiveness of Mission-time Linear Temporal Logic (MLTL) in AI Applications

Mission-time Linear Temporal Logic (MLTL) adds closed-interval integer bounds on the temporal operators of LTL, enabling unit-agnostic specification over finite traces. It is arguably the most-used variation of MTL, and the most-used subset of STL in industrial and AI applications. MLTL optimizes the trade-off between expressibility of a wide range of realistic requirements and the ability to author generic, easy-to-validate formulas. We highlight successful AI applications centered around MLTL requirements, including Robonaut2 and the NASA Lunar Gateway Vehicle System Manager. We overview advances in analyzing MLTL, explain the motivation driving these developments, and point out the gaps in the state of the art where there are needs for future work.

https://ltlf-symposium.github.io/invited/

Leave a Comment

Filed under Research Talks

OpenUAS Team Featured by Iowa Space Grant Consortium

https://www.linkedin.com/feed/update/urn:li:activity:7041839584405557248/?lipi=urn%3Ali%3Apage%3Ad_flagship3_detail_base%3BqprBn35zROmlfmXDlZXR6w%3D%3D

Leave a Comment

Filed under Laboratory Collaborations, News Features

Lab Alumni Zachary Luppen Announces Starlink 2-5 Launch for SpaceX

Image: SpaceX with automatically-generated captions (correct spelling: Luppen)

Watch the recording here: https://www.youtube.com/watch?v=JILQ2qe-cjI

Leave a Comment

Filed under Lab Alumni, News Features

[isabelle] New in the AFP: Stalnaker Logic

Stalnaker's Epistemic Logic
  by Laura P. Gamboa Guzman

This work is a formalization of Stalnaker's epistemic logic with countably many agents and its soundness and completeness theorems, as well as the equivalence between the axiomatization of S4 available in the Epistemic Logic theory and the topological one. It builds on the Epistemic Logic theory.


https://www.isa-afp.org/entries/Stalnaker_Logic.html

Leave a Comment

Filed under Laboratory Collaborations, Publication Highlights, Reproducibility

Inspiring tomorrow’s women in STEM

https://news.engineering.iastate.edu/2021/07/27/inspiring-tomorrows-women-in-stem-kristin-rozier/

Leave a Comment

Filed under Laboratory Collaborations, News Features, Outreach

Two Cyclone engineers receive NSF grant to create a smarter aircraft and spacecraft

https://news.engineering.iastate.edu/2020/10/22/two-cyclone-engineers-receive-nsf-grant-to-create-a-smarter-aircraft-and-spacecraft/

Leave a Comment

Filed under Awards, Laboratory Collaborations, News Features

Aerospace Engineering’s Rozier receives Black and Veatch Building a World of Difference in Engineering Fellowship

Aerospace Engineering’s Rozier receives Black and Veatch Building a World of Difference in Engineering Fellowship

Leave a Comment

Filed under Awards, News Features, Uncategorized

Rozier Presents Kempa with Teaching Excellence Award

Prof. Kristin Yvonne Rozier presents Ph.D. Candidate Brian Kempa with a Teaching Excellence (TEX) Award from Iowa State University.

From https://news.engineering.iastate.edu/2019/09/05/four-aerospace-engineering-graduate-students-receive-tex-rex-awards/

Kempa served as a teaching assistant for AerE 361 (Computational Techniques for Aerospace Design) for three semesters. AerE 361 is a required course with a coding component in the Department of Aerospace Engineering, and according to Rozier teaching of this course a special challenge due to technically-related issues in the past. Kempa volunteered to assist with the course while Rozier was in the process of overhauling the material, because he felt he had a valuable perspective from having taken the course as an undergraduate. Rozier nominated Kempa for his dedication and passion to teaching, which she called “truly exceptional.”

Leave a Comment

Filed under Uncategorized