1. Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geoffrey J. Gordon, and Peter Capell. Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges. Journal of Aerospace Information Systems, 11(10):702-713, 2014. Keyword(s): avionics, verification. Abstract:

   Complex software systems are becoming increasingly prevalent in aerospace applications: in particular, to accomplish critical tasks. Ensuring the safety of these systems is crucial, as they can have subtly different behaviors under slight variations in operating conditions. This paper advocates the use of formal verification techniques and in particular theorem proving for hybrid software-intensive systems as a well-founded complementary approach to the classical aerospace verification and validation techniques, such as testing or simulation. As an illustration of these techniques, a novel lateral midair collision-avoidance maneuver is studied in an ideal setting, without accounting for the uncertainties of the physical reality. The challenges that naturally arise when applying such technology to industrial-scale applications is then detailed, and proposals are given on how to address these issues.

   
   

   @article{ghorbalHybridTheoremProving2014,
   title = {Hybrid {{Theorem Proving}} of {{Aerospace Systems}}: {{Applications}} and {{Challenges}}},
   author = {Ghorbal, Khalil and Jeannin, Jean-Baptiste and Zawadzki, Erik and Platzer, Andr{\'e} and Gordon, Geoffrey J. and Capell, Peter},
   year = {2014},
   volume = {11},
   pages = {702--713},
   publisher = {{American Institute of Aeronautics and Astronautics}},
   doi = {10.2514/1.I010178},
   abstract = {Complex software systems are becoming increasingly prevalent in aerospace applications: in particular, to accomplish critical tasks. Ensuring the safety of these systems is crucial, as they can have subtly different behaviors under slight variations in operating conditions. This paper advocates the use of formal verification techniques and in particular theorem proving for hybrid software-intensive systems as a well-founded complementary approach to the classical aerospace verification and validation techniques, such as testing or simulation. As an illustration of these techniques, a novel lateral midair collision-avoidance maneuver is studied in an ideal setting, without accounting for the uncertainties of the physical reality. The challenges that naturally arise when applying such technology to industrial-scale applications is then detailed, and proposals are given on how to address these issues.},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4175-Ghorbal et al (2014) - Hybrid Theorem Proving of Aerospace Systems.pdf},
   journal = {Journal of Aerospace Information Systems},
   keywords = {avionics,verification},
   number = {10} 
   }
   




2. Conor Thomas McBride. How to Keep Your Neighbours in Order. ACM SIGPLAN Notices, 49(9):297-309, November 2014. ISSN: 0362-1340, 1558-1160. Keyword(s): Agda.
   

   @article{mcbrideHowKeepYour2014,
   title = {How to Keep Your Neighbours in Order},
   author = {McBride, Conor Thomas},
   year = {2014},
   month = nov,
   volume = {49},
   pages = {297--309},
   issn = {0362-1340, 1558-1160},
   doi = {10.1145/2692915.2628163},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4192-McBride (2014) - How to keep your neighbours in order.pdf},
   journal = {ACM SIGPLAN Notices},
   keywords = {Agda},
   number = {9} 
   }
   




3. Tobias Nipkow and Gerwin Klein. Abstract Interpretation. In Tobias Nipkow and Gerwin Klein, editors, Concrete Semantics: With Isabelle/HOL, pages 219-280. Springer International Publishing, Cham, 2014. ISBN: 978-3-319-10542-0. Keyword(s): abstract interpretation. Abstract:

   In Chapter 10 we saw a number of automatic program analyses, and each one was hand crafted. Abstract Interpretation is a generic approach to automatic program analysis. In principle, it covers all of our earlier analyses. In this chapter we ignore the optimizing program transformations that accompany certain analyses.

   
   

   @incollection{nipkowAbstractInterpretation2014,
   title = {Abstract {{Interpretation}}},
   booktitle = {Concrete {{Semantics}}: {{With Isabelle}}/{{HOL}}},
   author = {Nipkow, Tobias and Klein, Gerwin},
   editor = {Nipkow, Tobias and Klein, Gerwin},
   year = {2014},
   pages = {219--280},
   publisher = {{Springer International Publishing}},
   address = {{Cham}},
   doi = {10.1007/978-3-319-10542-0_13},
   abstract = {In Chapter 10 we saw a number of automatic program analyses, and each one was hand crafted. Abstract Interpretation is a generic approach to automatic program analysis. In principle, it covers all of our earlier analyses. In this chapter we ignore the optimizing program transformations that accompany certain analyses.},
   isbn = {978-3-319-10542-0},
   keywords = {abstract interpretation} 
   }
   

1. Gethin Norman and David Parker. Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance. Technical report, The London Mathematical Society and the Smith Institute, 2014. Keyword(s): model checking.
   

   @techreport{normanQuantitativeVerificationFormal2014,
   title = {Quantitative {{Verification}}: {{Formal Guarantees}} for {{Timeliness}}, {{Reliability}} and {{Performance}}},
   author = {Norman, Gethin and Parker, David},
   year = {2014},
   institution = {{The London Mathematical Society and the Smith Institute}},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4357-Norman_Parker (2014) - Quantitative Verification.pdf},
   keywords = {model checking} 
   }
   

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