铺子
发表于 2025-3-26 23:56:03
http://reply.papertrans.cn/88/8763/876212/876212_31.png
含铁
发表于 2025-3-27 03:44:17
Using Dependent Types to Certify the Safety of Assembly Code enforced by CCured, a source-level instrumentation tool that guarantees type safety in legacy C programs. We can therefore check that the x86 assembly code resulting from compilation with CCured is in fact type-safe.
placebo-effect
发表于 2025-3-27 05:21:49
The PER Model of Abstract Non-interferencenconstrained attacker models, which do not necessarily either observe all public information or ignore all private information. Finally, we show how abstract domain completeness can be used for enforcing the PER model of abstract non-interference.
strdulate
发表于 2025-3-27 12:06:20
Algorithmic Game Semantics and Static Analysisal in the tradition of denotational semantics, and has led to the cons truction of fully abstract models for programming languages incorporating a wide variety of features which have proved resistant to more tradition al approaches, including (combinations of): higher-order procedures, loca lly scop
extrovert
发表于 2025-3-27 17:27:39
From Typed Process Calculi to Source-Based Securityof C for buffer overruns is one approach. Another is to introduce . as a programming language feature so that the typechecker proves security properties; for example, languages like Jif and Flow Caml can check noninterference properties of application-level code. Independently, security types have a
良心
发表于 2025-3-27 20:50:06
http://reply.papertrans.cn/88/8763/876212/876212_36.png
后退
发表于 2025-3-28 01:45:48
http://reply.papertrans.cn/88/8763/876212/876212_37.png
挖掘
发表于 2025-3-28 05:54:52
Inference of Well-Typings for Logic Programs with Application to Termination Analysiseriving types from which norms can automatically be constructed. Previous work on type-based termination analysis used either types declared by the user, or automatically generated monomorphic types describing the success set of predicates. The latter types are less precise and result in weaker term
judiciousness
发表于 2025-3-28 07:28:06
Memory Space Conscious Loop Iteration Duplication for Reliable Executionchnology scales down. While hardware-based approaches to detect/correct soft errors are important, software-based techniques can be much more flexible. One simple software-based strategy would be full duplication of computations and data, and comparing the results of the corresponding original and d
blight
发表于 2025-3-28 13:40:37
Memory Usage Verification for OO Programsed to successfully execute methods that operate on these data structures. Key components of this type system include type assertions that use symbolic Presburger arithmetic expressions to capture data structure sizes, the effect of methods on the data structures that they manipulate, and the amount