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. Aditya Dhodapkar, Avery Smidt, Aaron Verkleeren, Carlos A. Varela, and Stacy Patterson. Predictive Sectorization and Bayesian Optimized Consensus for Autonomous Airspace Admission Control. In 2026 IEEE International Conference on Systems, Man, and Cybernetics (SMC), Bellevue, WA, USA, October 2026. IEEE. Keyword(s): air traffic control, airspace sectorization, machine learning, distributed consensus, bayesian optimization. Abstract:

   Conventional air traffic control divides airspace into specific regions, creating a scaling bottleneck as traffic grows. Choosing how to partition airspace is not straightforward because grid size affects workload, handoff frequency, and the capacity of whatever coordination mechanism operates within each sector. We present a three stage pipeline that automates sectorization and sector coordination while preserving human oversight. First, a two stage XGBoost classifier predicts the optimal 3D grid configuration from 23 location-agnostic traffic features, achieving 91.38% accuracy on a 65,000 sample dataset derived from Federal Aviation Administration System Wide Information Management replays. Second, a leaderless Paxos consensus protocol lets aircraft coordinate sector entries among themselves, maintaining above 96% entry success with low near mid-air collision rates across all tested configurations. Third, Bayesian Optimization with a Gaussian Process surrogate tunes eight protocol parameters per airport in 50 trials, revealing that each traffic environment requires a qualitatively different configuration. The resulting pipeline offers a practical path toward scalable, autonomous airspace management as traffic demand outpaces controller capacity.

   
   

   @inproceedings{dhodapkar-ieee-smc-2026,
   author = {Dhodapkar, Aditya and Smidt, Avery and Verkleeren, Aaron and Varela, Carlos A. and Patterson, Stacy},
   title = {Predictive Sectorization and {Bayesian} Optimized Consensus for Autonomous Airspace Admission Control},
   booktitle = {2026 IEEE International Conference on Systems, Man, and Cybernetics (SMC)},
   year = {2026},
   month = oct,
   address = {Bellevue, WA, USA},
   publisher = {IEEE},
   keywords = {air traffic control, airspace sectorization, machine learning, distributed consensus, bayesian optimization},
   pdf = "http://wcl.cs.rpi.edu/papers/IEEE_SMC-Final.pdf",
   abstract = {Conventional air traffic control divides airspace into specific regions, creating a scaling bottleneck as traffic grows. Choosing how to partition airspace is not straightforward because grid size affects workload, handoff frequency, and the capacity of whatever coordination mechanism operates within each sector. We present a three stage pipeline that automates sectorization and sector coordination while preserving human oversight. First, a two stage XGBoost classifier predicts the optimal 3D grid configuration from 23 location-agnostic traffic features, achieving 91.38% accuracy on a 65,000 sample dataset derived from Federal Aviation Administration System Wide Information Management replays. Second, a leaderless Paxos consensus protocol lets aircraft coordinate sector entries among themselves, maintaining above 96% entry success with low near mid-air collision rates across all tested configurations. Third, Bayesian Optimization with a Gaussian Process surrogate tunes eight protocol parameters per airport in 50 trials, revealing that each traffic environment requires a qualitatively different configuration. The resulting pipeline offers a practical path toward scalable, autonomous airspace management as traffic demand outpaces controller capacity. } 
   }
   




2. Siew Goh and Carlos A. Varela. Securing ADS-B with Byzantine Fault Tolerance: Towards A Formal Specification. In The 45th AIAA/IEEE Digital Avionics Systems Conference (DASC 2026), September 2026. Keyword(s): formal verification, ADS-B, Athena, Byzantine Agreement. Abstract:

   The Automatic Dependent Surveillance-Broadcast (ADS-B) protocol, widely used for air traffic surveillance, lacks built-in security mechanisms and is vulnerable to spoofing, data manipulation, and denial-of-service attacks. Addressing these vulnerabilities while preserving real-time performance requires fundamentally new approaches. This paper proposes a Byzantine fault-tolerant (BFT) consensus framework to secure ADS-B by constructing a trustworthy airspace view from potentially un trusted broadcast data. We define key aviation safety properties, including agreement, non-creation, and validity. We then adapt Practical Byzantine Fault Tolerance (PBFT) to aeronautical networks with dynamic committee membership and timing constraints. Using the Athena proof assistant, we present work in progress towards formalizing the system, by specifying its main safety and liveness properties.

   
   

   @InProceedings{goh-dasc-2026,
   author = {Siew Goh and Carlos A. Varela},
   title = {Securing ADS-B with Byzantine Fault Tolerance: Towards A Formal Specification},
   booktitle="The 45th AIAA/IEEE Digital Avionics Systems Conference (DASC 2026)",
   year="2026",
   month="September",
   pdf = {https://wcl.cs.rpi.edu/papers/goh_DASC2026.pdf},
   keywords = {formal verification, ADS-B, Athena, Byzantine Agreement},
   abstract = {The Automatic Dependent Surveillance-Broadcast (ADS-B) protocol, widely used for air traffic surveillance, lacks built-in security mechanisms and is vulnerable to spoofing, data manipulation, and denial-of-service attacks. Addressing these vulnerabilities while preserving real-time performance requires fundamentally new approaches. This paper proposes a Byzantine fault-tolerant (BFT) consensus framework to secure ADS-B by constructing a trustworthy airspace view from potentially un trusted broadcast data. We define key aviation safety properties, including agreement, non-creation, and validity. We then adapt Practical Byzantine Fault Tolerance (PBFT) to aeronautical networks with dynamic committee membership and timing constraints. Using the Athena proof assistant, we present work in progress towards formalizing the system, by specifying its main safety and liveness properties.} 
   }
   

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