%PDF-1.3
%
1 0 obj
<>
endobj
2 0 obj
<>stream
Ejecución simbólica
Automated Test Case Generation
Symbolic Execution
SAT/SMT
Test case generation
Symbolic Execution
Constraint satisfiability
Z3
Generació de casos de prova
Execució simbòlica
Satisfacibilitat de restriccions
SMT-Solvers
[ES] En Ingeniería de Software, el concepto de contrato está relacionado con una especificación del comportamiento de los programas utilizando descripciones que típicamente incluyen precondiciones y postcondiciones. El estado del arte actual permite generar automáticamente contratos a partir del código fuente que pueden ser usados como entrada para analizadores cada vez más potentes. Sin embargo, los contratos generados automáticamente pueden no ser completamente precisos o correctos, conteniendo algunos elementos que no están verificados. El objetivo de este proyecto es desarrollar una aplicación que permite refinar dichos contratos, utilizando el sistema resolutor SMT Z3 para identificar y eliminar aquellos componentes que el proceso de validación determina que son demostradamente falsos.
[EN] Software contracts provide formal specification for the terms of the service that software components can provide. Contracts on software are essentially written by using program preconditions and postconditions that formalize the mutual obligations and benefits of the software units or routines.
The current state of the art allows contracts to be automatically inferred from the source code so that can be used as input for increasingly powerful analyzers. However, automatically generated contracts can not be completely accurate or correct, containing some elements that are not verified. The goal of this project is to develop a software application that allows contracts to be refined by using the SMT solver Z3 to identify and eliminate those components that are proved to be false.
[CA] En Enginyeria de Software, el concepte de contracte està relacionat amb una
especificació del comportament dels programes utilitzant descripcions que típicament inclouen precondicions i postcondicions.
L’estat de l’art actual permet generar automàticament contractes a partir de
el codi font que poden ser usats com a entrada per a analitzadors cada vegada
més potents. No obstant això, els contractes generats automàticament poden no
ser completament precisos o correctes, contenint alguns elements que no estan
verificats.
L’objectiu d’aquest projecte és desenvolupar una aplicació que permet refinar aquests contractes, utilitzant el sistema resolutori SMT Z3 per identificar i
eliminar aquells components que el procés de validació determina que són demostradament falsos.
Reserva de todos los derechos
Abierto
María Alpuente Frasnedo
Alicia Villanueva García
http://hdl.handle.net/10251/149332
Español
endstream
endobj
3 0 obj
<>
endobj
6 0 obj
<>
endobj
7 0 obj
<>
endobj
9 0 obj
<>stream
xˮz
fHv""xb3y _QɈGucwu__&7-)N.%O|烈_~<?}2/
RJ۟]#\bu{X˧ip}z5Z]/}s|+OOs)/\_z\r]Kes,uAkwwo;"]:ܽy&ww.Kt{pMo<r@_:"nw> o^4]9 lwgEf䵶Qja_QfSnne15E_]N[Ώ2mjXW䂹g??X*kkQ)*NݮYܮ5/_Ü&wa^bѵ%QnB]}!{߽D6BVT[f&+.hG
Eͯ\tLB=w-̟}ĉ8mq1^kFˬIv~I<8%V)V.K .aX|
k(aM/8uCE~x<ڮX<>yq%on:C&qO\JN ^p=j_g&^e?sy?@>p _h]0 $g9}zkQ:h12
qnN&՛+8N(uU?j/*Fc-Eޢ]>?vQslʞouOH|?9OۏT܁IȤR*}:3*~p]|rCR)uYs
$g7/Y1/9KuEŷ1)4]J$h!\ibxSLR:i~w+h|]JU-O"W1?D=d]TpiIP*Mw?35酒^_RIQB?Bz&W?WadC;ƲS9[~HglxdKxQ
3P\7k9%"fAI@hɕUt1ԙ\Y? @1,3eٛ_al+Aatu(H0=GOFD"uLa2}el'fK
cpReYh8<-ҫXa7^F(d»Q@n$;[x.4-["{SEW1OHќyW'xD@ApIf"f>ܛw^|h+scCIj7(!73s(R*o\e[T|ͬ'L"Y?+&t4|Ea1~EdA{U3gcL_RM2R÷$[pWd QՏEr[Uc1*+Ξxjӕ;y0&g|%HvHS?[t$<[ ,]([LoڥG KOz]÷@&wK'\1T
pKB7(~LfVc?[beSH6?-^sCb.("K՝&QsVn.F*Թo0~|#U*j6TQ 9[TGsnVgU|()9&n&E?Q"}p[TwV,MQjK/)Jzb~҅]Y4v%GI}Dc*gюmZ,$=obxzu1^)njPـxD~jiƢ"ܳb4nИGEiu(tΨ3 ܭx,یݏAJ{+$>赗{.l>sYwoUO4εxwc:=a zj<^6CB̊00O%,bzReK-φn]wLc*@ŧ){eǖd'7aw_//>Ѿ$AZ7|Wv3gMW
8DId+Ηo~L+kBؓ_Ckz#;YCT/!'kT]P1>@__%[L_`U-sFLo2,v
[̮RdF蒎qQ)غ]=ca>tMe!dɏmoͳOVzy4|lPG))|Hm|X}k=$79-Mi_7 C8|rVO`qJb?㛄qobAxaae%QMTXd
x]A
G?NN }dkp9-*4}!ZA^g|9s?}:5ۛ>/ExtGState<>/Font<>/XObject<>>>
endobj
18 0 obj
[/ICCBased 29 0 R]
endobj
26 0 obj
<>
endobj
27 0 obj
<>stream
JFIF C
%# , #&')*)-0-(0%()( C
((((((((((((((((((((((((((((((((((((((((((((((((((( $" ^
!1"AQaq#2Rt367Bbrs45Cu$FUSc&'V%8DEG 1A!aq ? (WS
%;*X7$
kG*a=/I-ڵusҌ^owl(<=jnAq6||7휩5c^yMrnpTs[pDey~eR˯g#$J=t)֮͢e
ΚC0۩Z.¦+,v{-1,PH
8V1;{Pp]~Gtytm_ki骪=uglIz'g㱺
W/TٜZ7̟ F3\]3 6V`葽S#*ҚǩV7wwM/VQ""" """ """ """ """ """ """ """ """ """ """ """ """ """ """ """ """ """ """ """ """ ""ڴf;m,gO[@=Ds$uL]m{٠kIa53;dgzQi[[m{z(qd}>vټ-&أ-\<}A}ZҟQꋍAQBã36ys٬/ܔF5%
a̳pKga#Kn
/6i-#x<NJmJnֻ=-şd`sqM-KO#"ˮ;}cֹ*zJ;-ntρ2=P7Ap;G4%mUP/4Ȝe奎w(u{KEKz]h]{k@&٦w+=1+,[hG)ѬOTX(ۤU<1$@R/֚8:vU_H+|g74. Q]YGYxt->QenA'jmj}Om}-CjkG
; n{S1ͩcs8iQ
Efk_La[w5o'8Ꮼm>fv%JNX?$r8M?woc>vG;9֢Smp%Pjf9;^= A`Z$Z4 u>9+EA]!rMya""|1Şbl~=%{ϭt?ΥyCXMZ$zk$KMHlToqAg$+rwpx>Ku}-ʎ*QM($a*#%uVoP
Cwkwl' Ɂ<8Uۨ6Ir5_veǀpw8Ezݪm-KvHwp """ ""Mi;t}Q45-`8|B,|y7kجJѴ1QSCx+r0pFB/>Ai6va{P(Ֆ,g%|L.,aw"
|ߺ*VEpV砩3x`dpbi<2&кh>~Ӓ|-kppZ 䤫0myi6WQK#&HÇ11
Qt>i\[|v\MXZYTyeY]"8(T(Zq̎]A.ۡIP)@/˚;bpm'OV%jCiSZwz88ARQZ_aoS7Y9iHUiSmOާ`7ͥ{UO{/Qk/T$| 2P.FP[YtsZ\I8Q}xzJv<