The HAL Environment On-Line Page
The HD-Automata Laboratory (HAL) is an integrated tool set for the specification, verification and analysis of concurrent and distributed systems. The core of HAL are the HD-automata: they are used as a common format for the various history-dependant languages. The HAL environment includes modules which implement decision procedures to calculate behavioral equivalences, and modules which support v
KindSoftware: Simplify Theorem Prover
The Eclipse Plugin for the Simplify Theorem Prover is found at http://kind/products/opensource/Simplify/simplify-eclipse/updates/ The source code is found in Subversion at https://mobius.ucd.ie/repos/src/simplify An archive of all binary executables for various platforms is found at http://kind/products/opensource/archives/Simplify1.5.5.zip What is the future of Simplify? Simplify was written by
List of important publications in computer science - Wikipedia
1.2A Proposal for the Dartmouth Summer Research Project on Artificial Intelligence
SAFE Code
Static Analysis For safe Execution of Code SAFECode project aims at providing memory safety guarantees to programs written in unsafe languages like C and C++. As a part of this project, we developed a relatively simple compilation strategy that for standard C programs guarantees sound semantics for an aggressive interprocedural pointer analysis (or simpler ones), a call graph, and type information
Java String Analyzer
The Java String Analyzer is a tool for analyzing the flow of strings and string operations in Java programs. For each string expression, it computes a finite-state automaton that provides an upper approximation of the values that may appear at runtime. Read the paper: Precise Analysis of String Expressions [ abstract | PDF | BibTeX ] (in Proc. SAS'03) Download the source code or jar files If you w
RTOSライブラリ - Toshiaki Aoki's Home Page
μITRON RTOS用ライブラリ for PROmela/spiN (μIPRON) μIPRONは，「μITRON RTOS用ライブラリ for PROmela/spiN」の省略名です． 「マイクロアイプロン」と発音してください μIPRONはモデル検査ツールspinを用いて，μITRON仕様のRTOS(Real-Time Operating System)上で動作するマルチタスクソフトウェアを検証するためのライ ブラリです．Spinの入力言語では，μITRONなどのRTOSで使う優先度や sleep/wakeupなどの概念を直接的に記述することができません．そこで，これらの 概念が取り扱えるようなライブラリμIPRONを作りました．μIPRONでは，μITRON の挙動をpromela/spinでエミュレーションします．これにより，promelaでμITRON
Main Page - WalaWiki
Welcome to the T.J. Watson Libraries for Analysis (WALA) The T. J. Watson Libraries for Analysis (WALA) provide static analysis capabilities for Java bytecode and related languages and for JavaScript. The system is licensed under the Eclipse Public License, which has been approved by the OSI (Open Source Initiative) as a fully certified open source license. The initial WALA infrastructure was inde
Deep Web - kwakita’s diary
ご無沙汰してます。今月号の CACM から deep Web （以下、深層ウェブ）についての論文を紹介します。IPアドレスを乱択して得たウェブサイトのなかでバックエンドのデータベースを使って問い合わせをしているものを探すことで、ウェブ全体に存在する深層ウェブの数を推定しています。案外、検索エンジンが深層ウェブを見つけていることに驚きました。論文の最後に、深層ウェブをサポートするための方式についてちらりと提案していますが、よく分りません。同じ著者らがすでに書いた論文に書かれているようです。 B. He, M. Patel, Z. Zhang, and K. C.-C. Chang, "Accessing the Deep Web," CACM 50, 5 (2007), pp. 95-101. 深層ウェブの発見 原理的に有効な2,230,124,544個の IP アドレスから無作為に百万個を
Unifying events and threads
Project introduction: This project uses a language-based technique to unify two seemingly opposite programming models for building massively concurrent network services: the event-driven model and the multithreaded model. The result is a unified concurrency model providing both thread abstractions and event abstractions. We implemented the unified concurrency model in Haskell, a pure, lazy, fun
JTL - Ssdlpedia
JTL, (the Java Tools Language, pronounced "Gee-tel") is a high-level query language for selecting program elements. The language is designed to serve the development of source code software tools for Java, and for programming language extensions. Applications include definition of joinpoints for aspect-oriented programming, fixing type constraints for generic programming, specification of encapsul
募集要項（PD・DC2・DC1） | 特別研究員｜日本学術振興会
募集要項のホームページは リニューアルに伴いURLを変更致しました。 ブックマークをされている方はお手数ですが変更をお願いします。
Epigram
www.e-pig.org This is the homepage of the Epigram project. Epigram is a dependently typed programming language and an interactive programming environment. Epigram has got a type system which is strong enough to express the behaviour of programs, the type checker then guarantees that the program is well behaved. However, you don't have to go as far, you can write ordinary programs and refactor them
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
The CBMC Homepage
http://www.cs.unibo.it/~sangio/DOC_public/history_bis_coind.pdf
http://www.doc.ic.ac.uk/~rhu/sessiondj.html
http://www.daimi.au.dk/~martinm/CCSVisualizer.html/
PROFUNDIS
PURe - TWiki
DrHylo - Personal/Alcino - TWiki
Termination Competition'2007