No description available.

No description available.

Made available in DSpace on 2014-06-12T15:52:36Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Devido á grande demanda por softwares cada vez mais robustos, complexos e flexíveis, e, sobretudo, pelo curtíssimo tempo de entrega exigido, a engenharia de software tem procurado novos meios de desenvolvimento que supram satisfatoriamente essas demandas. Uma forma de galgar esses novos patamares de produtividade provém do uso de uma metodologia baseada em agentes que se comunicam e com isso, ao invés dos programas serem estritamente programados, o comportamento destes sistemas de software emerge da interação de agentes, robôs, ou subsistemas aut onomos, independentes, além de declarativamente especificados. Isto provê a habilidade para automaticamente configurá -los, otimizá-los, monitorá-los, adaptá-los, diagnosticá-los, repará-los e protegê-los dentro do ambiente. Contudo, um grande problema das linguagens declarativas é a falta de mecanismos que permitem a melhor estruturação de dados, facilitando portanto, o reuso. Portanto, esta dissertação explica o desenvolvimento de nova linguagem lógica declarativa para programar sistemas de raciocínio automático de uma forma modularizada: C2HR∨. A linguagem base escolhida para a extensão com componentes lógicos foi CHR. Os motivos para essa escolha são definidos ao longo da dissertação. Duas abordagens, portanto, são apresentadas: a primeira, conhecida como CHRat, foi desenvolvida numa parceria juntamente com o grupo de pesquisas CONTRAINTES do INRIA/Rocquencourt-Paris, onde o programador ´e o responsável direto por definir os componentes CHR, permitindo o seu reuso por outros componentes; a segunda aplicação, CHRtp, visa atender prioritariamente requisitos de completude e, por isso, se baseia em procedimentos lógicos de inferência como: o raciocínio para frente, o raciocínio para trás, e a resolução/factoring. A dissertação mostra também alguns exemplos práticos, onde uso de componentes facilita radicalmente sua implementação. As contribuições almejadas com essa dissertação são: a definição de uma família bem formalizada de provadores de teoremas automáticos, que podem trabalhar com sentenças especificadas em lógica horn ou em lógica de primeira ordem, a extensão de CHR como uma linguagem modular de propósito geral, a melhor estruturação de bases conhecimentos e até o uso em conjunto de bases heterogêneas, a definição de uma linguagem para a fácil e direta estruturação de dados por meio de componentes, dentre outras

No description available.

Formal methods play a significant and increasing role in hardware verification, but their effectiveness can be impaired by the ac hoc nature of mainstream hardware languages such as VHDL, Verilog and SystemC, which have convoluted semantics that often necessitate contrived proof techniques. This dissertation investigates the application of formal reasoning to hardware architectures expressed in an alternative class of semantically elegant languages, which support efficient design, whilst also having been developed with proof techniques in mind. A network-on-chip architecture belonging to the SpiNNaker many-core processor is specified in Concurrent Haskell, and a hand proof is presented which verifies a novel routing mechanism by mathematical induction. A subset of Bluespec SystemVerilog (BSV) is embedded in the higher order logic of the PVS theorem prover. Owing to the clean semantics of BSV, application of monadic techniques leads to a surprisingly elegant embedding, in which hardware designs are translated into logic almost verbatim, preserving types and language constructs. Proof strategies are written in the PVS strategy language; these automatically verify temporal logic theorems concerning the resulting monadic expressions, by employing a combination of model checking and deductive reasoning. The subset of BSV which is embedded includes module definition and instantiation, methods, implicit conditions, scheduling attributes, and rule composition using methods from instantiated modules. The aforementioned subset of BSV is also embedded in the specification language of the SAL model checker, and a verification strategy is presented which combines the specialised model checking capabilities of SAL with the diverse proof strategies of PVS.

Automated Theorem Provers (ATP) are software programs which carry out inferences over logico-mathematical systems, often with the goal of finding proofs to some given theorem. ATP systems are enormously powerful computer programs, capable of solving immensely difficult problems. Currently, many automated theorem provers exist like E, vampire, SPASS, ACL2, Coq etc. However, all the available theorem provers have some common problems: (1) Current ATP systems tend not to try to find proofs entirely on their own. They need help from human experts to supply lemmas, guide the proof, etc. (2) There is not a single proof system available which provides fully automated platforms for both First Order Logic (FOL) and other Higher Order Logic (HOL). (3) Finally, current proof systems do not have an easy way to quickly deploy and reason over new logical systems, which a logic researcher may want to test. In response to these problems, I introduce the MATR framework. MATR is a platform-independent, codelet-based (independently operating processes) proof system with an easy-to-use Graphical User Interface (GUI), where multiple codelets can be selected based on the formal system desired. MATR provides a platform for different proof strategies like deduction and backward reasoning, along with different formal systems such as non-classical logics. It enables users to design their own proof system by selecting from the list of codelets without needing to write an ATP from scratch.

No description available.

<p>Interval arithmetic is used to enclose roundoff, truncation, and modeling errors in interval methods, thus obtaining numerical methods with automatic verification of the results. The Fundamental Theorem of Interval Arithmetic (FTIA) shows that, when evaluating an expression using interval arithmetic, the computed result contains the mathematically correct value of the expression.</p> <p>Decorations were introduced in the IEEE P1788 working group for standardizing interval arithmetic. Their role is to help track properties of interval evaluations. That is, we wish to say if a function is defined, undefined, or continuous in its inputs. Moreover, decorations act as local exception flags and do not lead to interruption of the computations. The FTIA plus the decoration system is expanded into the Fundamental Theorem of Decorated Interval Arithmetic (FTDIA).</p> <p>Several versions of this theorem are formulated and proved by J. Pryce. This thesis formalizes and proves the core of this theorem (version 3.0 of the IEEE-P1788 proposal) using the theorem prover Coq. Namely, we prove it for the common case where all the inputs to a function are non-empty intervals.</p> <p>There are two distinctive features of our formalization and proof. First, we define the semantics of an interval as a set of real numbers (including the empty set), and we do not impose any other restrictions on such a set, except that models of this interval can decide if the set is empty or not. For example, an interval need not be closed and bounded, as in traditional interval arithmetic. Second, our formalization and proof do not rely on specific interval operations: it works with any interval operation that satisfies the requirements for decorated interval library operations.</p> <p>As the FTDIA is central to the IEEE-P1788 proposal, the correctness of the FTDIA is crucial. Our mechanized proof can give the research community in interval computations much confidence in its correctness. The current version of the FTDIA (in P1788 version 8.0) is slightly different from the theorem proved here. Modifying our proof to reflect this is left as future work.</p> / Doctor of Philosophy (PhD)

Answer set programming (ASP) is a declarative approach to solving search problems. Logic programming constitutes the foundation of ASP. ASP is not a proof-theoretical approach where you get solutions by answer substitutions. Instead, the problem is represented by a logic program in such a way that models of the program according to the answer set semantics correspond to solutions of the problem. Answer set solvers (Smodels, Cmodels, Clasp, and Dlv) are used for finding answer sets of a given program. Although users can write programs with variables for convenience, current answer set solvers work on ground logic programs where there are no variables. The grounding step of ASP generates a propositional instance of a logic program with variables. It may generate a huge propositional instance and make the search process of answer set solvers more difficult. Model generation theorem provers (Paradox, Darwin, and FM-Darwin) have the capability of producing a model when the first-order input theory is satisfiable. This work proposes the use of model generation theorem provers as computational engines for ASP. The main motivation is to eliminate the grounding step of ASP completely or to perform it more intelligently using the model generation system. Additionally, regardless of grounding, model generation systems may display better performance than the current solvers. The proposed method can be seen as lifting SAT-based ASP, where SAT solvers are used to compute answer sets, to the first-order level for tight programs. A completion procedure which transforms a logic program to formulas of first-order logic is utilized. Besides completion, other transformations which are necessary for forming a firstorder theory suitable for model generation theorem provers are investigated. A system called Completor is implemented for handling all the necessary transformations. The empirical results demonstrate that the use of Completor and the theorem provers together can be an eective way of computing answer sets. Especially, the run time results of Paradox in the experiments has showed that using Completor and Paradox together is favorable compared to answer set solvers. This advantage has been more clearly observed for programs with large propositional instances, since grounding can be a bottleneck for such programs.

abstract: Computer science education is an increasingly vital area of study with various challenges that increase the difficulty level for new students resulting in higher attrition rates. As part of an effort to resolve this issue, a new visual programming language environment was developed for this research, the Visual IoT and Robotics Programming Language Environment (VIPLE). VIPLE is based on computational thinking and flowchart, which reduces the needs of memorization of detailed syntax in text-based programming languages. VIPLE has been used at Arizona State University (ASU) in multiple years and sections of FSE100 as well as in universities worldwide. Another major issue with teaching large programming classes is the potential lack of qualified teaching assistants to grade and offer insight to a student’s programs at a level beyond output analysis. In this dissertation, I propose a novel framework for performing semantic autograding, which analyzes student programs at a semantic level to help students learn with additional and systematic help. A general autograder is not practical for general programming languages, due to the flexibility of semantics. A practical autograder is possible in VIPLE, because of its simplified syntax and restricted options of semantics. The design of this autograder is based on the concept of theorem provers. To achieve this goal, I employ a modified version of Pi-Calculus to represent VIPLE programs and Hoare Logic to formalize program requirements. By building on the inference rules of Pi-Calculus and Hoare Logic, I am able to construct a theorem prover that can perform automated semantic analysis. Furthermore, building on this theorem prover enables me to develop a self-learning algorithm that can learn the conditions for a program’s correctness according to a given solution program. / Dissertation/Thesis / Doctoral Dissertation Computer Science 2020