Rigorous Software Development: An Introduction to Program Verification
暫譯: 嚴謹的軟體開發：程式驗證入門

José Bacelar Almeida is a lecturer at the University of Minho, Portugal. He graduated in Electrical and Computer Engineering and received his PhD in Computer Science from the University of Minho. His areas of interest include semantics of programming languages, proof assistants, and security. Maria João Frade obtained her PhD in Computer Science from the University of Minho, Portugal, and is currently a lecturer at this institution. Her research interests include type theory, structural proof theory, semantics of programming languages and program logics. Jorge Sousa Pinto obtained his PhD in Computer Science from École Polytechnique, France, and is currently a lecturer at the University of Minho, Portugal. His interests include program verification and the use of formal methods in software engineering. Simão Melo de Sousa is a lecturer at the University of Beira Interior, Portugal. He graduated in Computer Science from the University of Orléans, France, and received his PhD in ComputerScience from the University of Nice-Sophia Antipolis / INRIA. His interests include formal methods, reliability and security of computer systems, and computer-aided reasoning.

何塞·巴塞拉·阿爾梅達（José Bacelar Almeida）是葡萄牙米尼奧大學的講師。他畢業於電機與計算機工程，並在米尼奧大學獲得計算機科學博士學位。他的研究興趣包括程式語言的語義、證明輔助工具和安全性。瑪麗亞·若昂·弗拉德（Maria João Frade）在葡萄牙米尼奧大學獲得計算機科學博士學位，目前是該機構的講師。她的研究興趣包括類型理論、結構證明理論、程式語言的語義和程式邏輯。豪爾赫·蘇薩·平托（Jorge Sousa Pinto）在法國高等工藝學院（École Polytechnique）獲得計算機科學博士學位，目前是葡萄牙米尼奧大學的講師。他的興趣包括程式驗證和在軟體工程中使用形式方法。西滿·梅洛·德·蘇薩（Simão Melo de Sousa）是葡萄牙比拉內特大學的講師。他畢業於法國奧爾良大學的計算機科學，並在尼斯-索非亞·安提波利斯大學/法國國家資訊與自動化研究所（INRIA）獲得計算機科學博士學位。他的興趣包括形式方法、計算機系統的可靠性和安全性，以及計算機輔助推理。