A Logical Characterization of Forward and Backward Chaining in the Inverse Method [0.03%]
逆向方法中前向链和后向链的逻辑刻画
Kaustuv Chaudhuri; Frank Pfenning; Greg Price
Kaustuv Chaudhuri; Frank Pfenning; Greg Price
Raúl Monroy; Alan Bundy; Ian Green
Raúl Monroy; Alan Bundy; Ian Green
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads [0.03%]
使用硬件中断和抢占式线程对低级程序进行认证
Xinyu Feng; Zhong Shao; Yu Guo; Yuan Dong
Xinyu Feng; Zhong Shao; Yu Guo; Yuan Dong
Volker Haarslev; Ralf Möller
Volker Haarslev; Ralf Möller
Proving Fairness and Implementation Correctness of a Microkernel Scheduler [0.03%]
微内核调度器的公平性与实现正确性证明
Matthias Daum; Jan Dörrenbächer; Burkhart Wolff
Matthias Daum; Jan Dörrenbächer; Burkhart Wolff
Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code [0.03%]
针对C代码的跨过程且流敏感的类型分析，以确保内存和类型安全
Syrine Tlili; Mourad Debbabi
Syrine Tlili; Mourad Debbabi
María del Mar Gallardo; Pedro Merino; David Sanán
María del Mar Gallardo; Pedro Merino; David Sanán
An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps [0.03%]
在Coq中基于组合超图形式化的一个离散版乔丹曲线定理的直觉主义证明
Jean-François Dufourd
Jean-François Dufourd
Formal Memory Models for the Verification of Low-Level Operating-System Code [0.03%]
用于低级操作系统代码验证的形式化内存模型
Hendrik Tews; Marcus Völp; Tjark Weber
Hendrik Tews; Marcus Völp; Tjark Weber
Bishop Brock; Matt Kaufmann; J Strother Moore
Bishop Brock; Matt Kaufmann; J Strother Moore