- -

Listar por palabra clave "Symbolic execution"

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Listar por palabra clave "Symbolic execution"

Ordenar por:Orden:Resultados:

  • thumb
    Abstract Contract Synthesis and Verification in the Symbolic K Framework 
    Alpuente Frasnedo, María; Pardo Pont, Daniel; Villanueva García, Alicia (Universitat Politècnica de València, 2018-04-12)
    [EN] In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based ...
  • thumb
    Abstract Contract Synthesis and Verification in the Symbolic K Framework 
    Alpuente Frasnedo, María; Pardo, Daniel; Villanueva, Alicia (IOS Press, 2020)
    [EN] In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNELC, that supports pointer-based ...
  • thumb
    Automatic inference of specifications using matching logic 
    Alpuente Frasnedo, María; Feliú Gabaldón, Marco Antonio; Villanueva García, Alicia (Association for Computing Machinery (ACM), 2013-01-21)
    Formal specifications can be used for various software engineering activities ranging from finding errors to documenting software and automatic test-case generation. Automatically discovering specifications for heap-manipulating ...
  • thumb
    Concolic Testing in Logic programming 
    Mesnard, Fred; Payet, Etienne; Vidal Oriola, Germán Francisco (Cambridge University Press, 2015-07)
    Software testing is one of the most popular validation techniques in the software industry. Surprisingly, we can only find a few approaches to testing in the context of logic programming. In this paper, we introduce a ...
  • thumb
    Ejecución simbólica como herramienta de análisis 
    Pardo Pont, Daniel (Universitat Politècnica de València, 2015-03-25)
    [ES] El análisis automático de software permite verificar que un programa cumpla una serie de propiedades deseables sin intervención humana, aportando agilidad al proceso de ingeniería y reduciendo los riesgos del software ...
  • thumb
    Generación de trazas para la ejecución concólica de programas Erlang 
    Coll Ruiz, Onofre (Universitat Politècnica de València, 2016-05-17)
    [EN] A system for testing Erlang applications using concolic execution has been proposed. Matem
  • thumb
    Inferencia de especificaciones para programas C 
    Pardo Pont, Daniel (Universitat Politècnica de València, 2016-07-20)
    [EN] Despite its many unquestionable benefits, formal specifications are not widely used in industrial software development. In order to reduce the time and effort required to write formal specifications, in this Master ...
  • thumb
    Symbolic execution as a basis for termination analysis 
    Vidal Oriola, Germán Francisco (Elsevier, 2015-05)
    Program termination is a relevant property that has been extensively studied in the context of many different formalisms and programming languages. Traditional approaches to proving termination are usually based on ...