1. Jose Meseguer, Carlos A. Varela, and Nalini Venkatasubramanian, editors. Concurrent Programming, Open Systems and Formal Methods: Essays Dedicated to Gul Agha to Celebrate His Scientific Career, volume 16120 of Lecture Notes in Computer Science. Springer Nature Switzerland, 2026. Abstract:

   This Festschrift is dedicated to Gul Agha in recognition of his outstanding research and teaching impact. Gul Agha received his undergraduate degree at Caltech in 1977 and his A.M., M.S. and Ph.D. degrees at the University of Michigan, Ann Arbor. His thesis led to the MIT Press book Actors: A Model of Concurrent Computation in Distributed Systems, a work cited nearly 5000 times. After researcher and lecturer appointments at MIT and Yale, he moved to the University of Illinois, Urbana-Champaign, where he started as an assistant professor in 1989 and subsequently become a full professor and the founding director of the Open Systems Laboratory. The team's goal is to develop concurrent programming languages and systems that support applications with high-performance, fault-tolerance or real-time requirements, and this work has been very influential across domains such as Software Engineering, Formal Methods, Programming Languages, Concurrency Theory, Distributed Systems, and Cyber-Physical Systems. Gul Agha is a Fellow of the IEEE and a Fellow of the ACM, other honors include the IBM Faculty Award, the ONR Young Investigator Award, and the ACM Recognition of Service Award. Over the course of his career Gul has been a highly impactful mentor, and he has collaborated in research and in publications with a wide range of scientists and engineers, in academia and in industry. Beyond his deep expertise, they have been inspired by his well-rounded intellect, philosophy of life, and sense of humor, and their successes are reflected in the papers contributed to this volume.

   
   

   @Book{meseguer-lncs-2026,
   editor="Meseguer, Jose and Varela, Carlos A. and Venkatasubramanian, Nalini",
   title="Concurrent Programming, Open Systems and Formal Methods: Essays Dedicated to Gul Agha to Celebrate His Scientific Career",
   publisher="Springer Nature Switzerland",
   year="2026",
   url="https://doi.org/10.1007/978-3-032-05291-9",
   volume="16120",
   abstract="This Festschrift is dedicated to Gul Agha in recognition of his outstanding research and teaching impact. Gul Agha received his undergraduate degree at Caltech in 1977 and his A.M., M.S. and Ph.D. degrees at the University of Michigan, Ann Arbor. His thesis led to the MIT Press book Actors: A Model of Concurrent Computation in Distributed Systems, a work cited nearly 5000 times. After researcher and lecturer appointments at MIT and Yale, he moved to the University of Illinois, Urbana-Champaign, where he started as an assistant professor in 1989 and subsequently become a full professor and the founding director of the Open Systems Laboratory. The team's goal is to develop concurrent programming languages and systems that support applications with high-performance, fault-tolerance or real-time requirements, and this work has been very influential across domains such as Software Engineering, Formal Methods, Programming Languages, Concurrency Theory, Distributed Systems, and Cyber-Physical Systems. Gul Agha is a Fellow of the IEEE and a Fellow of the ACM, other honors include the IBM Faculty Award, the ONR Young Investigator Award, and the ACM Recognition of Service Award. Over the course of his career Gul has been a highly impactful mentor, and he has collaborated in research and in publications with a wide range of scientists and engineers, in academia and in industry. Beyond his deep expertise, they have been inspired by his well-rounded intellect, philosophy of life, and sense of humor, and their successes are reflected in the papers contributed to this volume.",
   series="Lecture Notes in Computer Science" 
   }
   

1. Carlos A. Varela. The AMST Language: Formal Verification and Execution of Actor Systems, pages 36-59. Springer Nature Switzerland, Cham, 2026. ISBN: 978-3-032-05291-9. Abstract:

   We formalize Agha, Mason, Smith, and Talcott's actor language (AMST)[2] using the Athena proof assistant[3]. Since Athena is a dual deduction and computation language, we can both rigorously prove formal properties of actor systems, as well as synthesize executable actor code from the theory.

   
   

   @Inbook{varela-lncs-2026,
   author="Varela, Carlos A.",
   editor="Meseguer, Jose and Varela, Carlos A. and Venkatasubramanian, Nalini",
   title="The AMST Language: Formal Verification and Execution of Actor Systems",
   bookTitle="Concurrent Programming, Open Systems and Formal Methods: Essays Dedicated to Gul Agha to Celebrate His Scientific Career",
   year="2026",
   publisher="Springer Nature Switzerland",
   address="Cham",
   pages="36--59",
   abstract="We formalize Agha, Mason, Smith, and Talcott's actor language (AMST)[2] using the Athena proof assistant[3]. Since Athena is a dual deduction and computation language, we can both rigorously prove formal properties of actor systems, as well as synthesize executable actor code from the theory.",
   isbn="978-3-032-05291-9",
   doi="10.1007/978-3-032-05291-9_2",
   url="https://doi.org/10.1007/978-3-032-05291-9_2",
   pdf = "http://wcl.cs.rpi.edu/papers/varela-lncs-2026.pdf" 
   }
   

1. Dylan Le, Joel McCandless, Carlos A. Varela, and Radoslav Ivanov. Verification of Autonomous Systems with Optimal Controllers. Technical report, Rensselaer Polytechnic Institute, Department of Computer Science, April 2026. Note: Invited Paper to IEEE Conference on Decision and Control (CDC) 2026. Keyword(s): formal verification, autonomous systems, optimal control, reachability analysis, gradient descent. Abstract:

   This paper considers the problem of reachability analysis of control systems with optimal controllers, as a first step towards verifying the safety and correctness of such systems. Despite their appeal in guaranteeing task satisfaction through cost minimization, optimal controllers are often challenging to assure. In particular, as system dynamics grow in complexity, solving the resulting optimization problem may be difficult, especially given time and computation constraints on real platforms. Thus, it is essential to verify that, even if the optimal solution is not always found, such controllers still accomplish the high-level control objective. In this paper, we focus on gradient descent algorithms and design a reachability algorithm by treating gradient descent as a separate (digital) dynamical system, embedded in the original (physical) dynamical system, with controls as part of the state. We evaluate the feasibility of the proposed method on two control systems, a two-dimensional quadrotor and a cartpole.

   
   

   @TechReport{le-mccandless-varela-ivanov-verification-2026,
   author = {Dylan Le and Joel McCandless and Carlos A. Varela and Radoslav Ivanov},
   title = {Verification of Autonomous Systems with Optimal Controllers},
   institution = {Rensselaer Polytechnic Institute, Department of Computer Science},
   year = 2026,
   month = April,
   pdf = {http://wcl.cs.rpi.edu/papers/cdc2026_techRep.pdf},
   keywords = {formal verification, autonomous systems, optimal control, reachability analysis, gradient descent},
   abstract = {This paper considers the problem of reachability analysis of control systems with optimal controllers, as a first step towards verifying the safety and correctness of such systems. Despite their appeal in guaranteeing task satisfaction through cost minimization, optimal controllers are often challenging to assure. In particular, as system dynamics grow in complexity, solving the resulting optimization problem may be difficult, especially given time and computation constraints on real platforms. Thus, it is essential to verify that, even if the optimal solution is not always found, such controllers still accomplish the high-level control objective. In this paper, we focus on gradient descent algorithms and design a reachability algorithm by treating gradient descent as a separate (digital) dynamical system, embedded in the original (physical) dynamical system, with controls as part of the state. We evaluate the feasibility of the proposed method on two control systems, a two-dimensional quadrotor and a cartpole.},
   note = {Invited Paper to IEEE Conference on Decision and Control (CDC) 2026.} 
   }
   

1. Aditya Dhodapkar. Predictive Sectorization and Bayesian Optimized Consensus for Admission Control in Autonomous Airspace Operations. Master's thesis, Rensselaer Polytechnic Institute, March 2026. Keyword(s): sectorization, consensus protocols, bayesian optimization, autonomous decision making, decentralized systems. Abstract:

   Modern air traffic management distributes authority across many controllers and facilities, but within each sector a single controller is the sole authority for separation and sequencing. As traffic volumes grow and next generation concepts such as NASA's Advanced Air Mobility push toward increasingly autonomous flight, this per sector human dependency becomes a scaling bottleneck. This thesis explores a multi stage pipeline for adaptive airspace sectorization and decentralized admission control that can reduce per sector workload without removing human oversight. We begin by simulating replays of real FAA SWIM flight plan trajectories across a three dimensional discretized airspace grid. A two stage XGBoost predictor trained on scored partitions first determines whether sectorization is needed, then states the optimal grid configuration. The predicted grid defines sector boundaries that are handed to a Paxos based consensus protocol, in which the aircraft coordinate sector transitions. A Bayesian optimization loop driven by a Gaussian Process surrogate searches for configurations that maximize entry success rate while rejecting any setting that produces a near mid air collision. Results show that the predictor reliably selects appropriate grid configurations across diverse traffic conditions, the consensus protocol maintains high entry success rates as traffic scales, and Bayesian Optimization discovers that each operating environment requires qualitatively different protocol tuning.

   
   

   @MastersThesis{dhodaa_thesis,
   author = {Aditya Dhodapkar},
   title = {Predictive Sectorization and Bayesian Optimized Consensus for Admission Control in Autonomous Airspace Operations},
   school = {Rensselaer Polytechnic Institute},
   year = 2026,
   month = {Mar},
   pdf = "http://wcl.cs.rpi.edu/theses/dhodaa_thesis.pdf",
   keywords = "sectorization, consensus protocols, bayesian optimization, autonomous decision making, decentralized systems",
   abstract = {Modern air traffic management distributes authority across many controllers and facilities, but within each sector a single controller is the sole authority for separation and sequencing. As traffic volumes grow and next generation concepts such as NASA's Advanced Air Mobility push toward increasingly autonomous flight, this per sector human dependency becomes a scaling bottleneck. This thesis explores a multi stage pipeline for adaptive airspace sectorization and decentralized admission control that can reduce per sector workload without removing human oversight. We begin by simulating replays of real FAA SWIM flight plan trajectories across a three dimensional discretized airspace grid. A two stage XGBoost predictor trained on scored partitions first determines whether sectorization is needed, then states the optimal grid configuration. The predicted grid defines sector boundaries that are handed to a Paxos based consensus protocol, in which the aircraft coordinate sector transitions. A Bayesian optimization loop driven by a Gaussian Process surrogate searches for configurations that maximize entry success rate while rejecting any setting that produces a near mid air collision. Results show that the predictor reliably selects appropriate grid configurations across diverse traffic conditions, the consensus protocol maintains high entry success rates as traffic scales, and Bayesian Optimization discovers that each operating environment requires qualitatively different protocol tuning.} 
   }
   

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Les documents contenus dans ces répertoires sont rendus disponibles par les auteurs qui y ont contribué en vue d'assurer la diffusion à temps de travaux savants et techniques sur une base non-commerciale. Les droits de copie et autres droits sont gardés par les auteurs et par les détenteurs du copyright, en dépit du fait qu'ils présentent ici leurs travaux sous forme électronique. Les personnes copiant ces informations doivent adhérer aux termes et contraintes couverts par le copyright de chaque auteur. Ces travaux ne peuvent pas être rendus disponibles ailleurs sans la permission explicite du détenteur du copyright.

This document was translated from BibT_EX by bibtex2html