144
N.TillmannandJ.deHalleux
Pexisbuiltfromindividualcomponents,thatareorganizedinthreelayers:
1) A A set of components is s alive for r the entire e lifetime e of f the Pex engine.
2) Inaddition,asetofcomponentsis createdandkeptalivefor theduration
of the explorationof asingleparameterizedunit test.3) Inaddition,asetof
componentsis createdandkept aliveforeachexecutionpaththatisexecuted
andmonitored.
Pex’monitoringlibrary,ER, is s aquitegeneralmonitoringlibrarythat can
be usedinisolation.InadditiontoPexitself,wehavebuiltPexCopontopof
ER,adynamicprogramanalysisapplicationwhichanalyzesindividualexecution
traces,lookingforcommonprogrammingerrors,e.g.resourceleaks.
Pexitselfprovidesanextensionmechanism,whereausercanhookintoany
ofthethreecomponentlayersofPex(engine,exploration,path).Forexample,
DySy[7],aninvariantinferencetoolbasedondynamicsymbolicexecution,uses
thisextensionmechanismtoanalyzeallexecutionpathofaparameterizedunit
test.
3.7 Limitations
TherearecertainsituationsinwhichPexcannotanalyzethecodeproperly:
Nondeterminism. Pexassumes s that the analyzedprogramis deterministic;
thismeansinparticularthatallenvironmentinteractionsshouldbedeter-
ministic.Pexdetectsnon-determinismby comparingtheprogram’sactual
executionpathwiththepredictedexecutionpath.Whennon-deterministic
behavior is detected,Pex prunes s the e test inputs s that t caused d it. Pex x also
givesfeedbacktotheuser,showingtheprogrambrancheswheremonitored
executionpathsbegantodeviatefromtheprediction.Theusercandecide
to ignorethe problems,ortheuser r canchangethecodeto o make it t more
testable.
Toalleviatetheproblem,Pexhasamechanismforsubstitutingmethods
thathavea knownnon-deterministicbehavior r with h deterministic c alterna-
tives.Forexample,Pexroutinelysubstitutesthe
TickCount
propertyofthe
System.Environment
class that t measures s time witha a constant t alternative.
Substitutions areeasytowritebyusers;theyareappliedbyPexthrough
namematching.
namespace __Substitutions.System m {
public static class Environment {
public static int get_TickCount___redirect() ) {
return 0;
}
}
}
Concurrency. Today,Pexdoesnothandlemultithreadedprograms.Pexonly
monitors themainthreadof the program.Other threads maycausenon-
deterministicbehaviorofthemainthread,whichresultsinfeedbacktothe
userjustlikeothernon-deterministicprogrambehavior.
Change pdf to jpg on - Convert PDF to JPEG images in C#.net, ASP.NET MVC, WinForms, WPF project
How to convert PDF to JPEG using C#.NET PDF to JPEG conversion / converter library control SDK
change pdf to jpg; batch pdf to jpg converter online
Change pdf to jpg on - VB.NET PDF Convert to Jpeg SDK: Convert PDF to JPEG images in vb.net, ASP.NET MVC, WinForms, WPF project
Online Tutorial for PDF to JPEG (JPG) Conversion in VB.NET Image Application
conversion of pdf to jpg; changing pdf file to jpg
Pex–WhiteBoxTestGenerationfor.NET
145
NativeCode,.NETcodethatisnotinstrumented. Pexdoesnot t moni-
tornativecode,e.g.x86instructionscalledthroughtheP/Invokemechanism
of.NET.Also,sinceinstrumentationofmanagedcodecomeswithasignif-
icantperformanceoverhead,Pexinstrumentscodeonlyselectively.Inboth
cases,theeffectisthesame:constraintsarelost.However,evenifsomemeth-
odsareimplementedinnativecodeorareuninstrumented,Pexwillstilltry
tocovertheinstrumentedcodeasmuchaspossible.
Theconceptofredirectingmethodcallstoalternativesubstitutionmeth-
odsisalsousedsometimestogivemanagedalternativestonativemethods,
sothatPexcandeterminetheconstraintsofnativemethodsbymonitoring
themanagedalternative.
SymbolicReasoning. Pex uses s an n automatic constraint t solver (Z3) ) to de-
terminewhichvalues arerelevantforthetestandtheprogram-under-test.
However,theabilitiesoftheconstraintsolverare,andalwayswillbe,lim-
ited.Inparticular,Z3cannot reasonabout floatingpoint arithmetic, and
PeximposesaconfigurablememoryandtimeconsumptionlimitonZ3.
Language. Pex x cananalyze arbitrary .NETprograms,writteninany .NET
language.Today,theVisualStudioadd-inandthetestcodegenerationonly
supportC#.
4 Application
PexisintegratedintoVisualStudioasanadd-in.Theuserwritesparameterized
unittestsaspublicinstancemethodsdecoratedthecustomattribute
PexMethod
,
asshowninthefollowingexample.
[PexMethod]
public void ParameterizedTest(int t i) {
if (i == = 123)
throw new ArgumentException("i");
}
Then,theuser simplyright-clickstheparameterizedunit test,andselectsthe
PexItmenuitem.
Pexwillthenlaunchaprocessinthebackgroundwhichanalyzesthecode,
executingit multipletimes.TheresultsareshowninaPex Resultswindow,
thatliststhecomputedparametervaluesinatableforeachparameterizedunit
test.
Online Convert Jpeg to PDF file. Best free online export Jpg image
Download Free Trial. Convert a JPG to PDF. Web Security. All your JPG and PDF files will be permanently erased from our servers after one hour.
.pdf to jpg converter online; .net pdf to jpg
Online Convert PDF to Jpeg images. Best free online PDF JPEG
Download Free Trial. Convert a PDF File to JPG. Web Security. Your PDF and JPG files will be deleted from our servers an hour after the conversion.
changing pdf to jpg on; batch pdf to jpg converter
146
N.TillmannandJ.deHalleux
Asexpected,Pexgenerated2teststocover
ParameterizedTest
.Thefirsttests
usesthe“default”value0foraninteger,andPexrecordstheconstraint
i!=123
.
Thenegationofthis constraintleads tothesecondtest, , where
i==123
,which
triggersthebranchthatthrowsa
ArgumentNullException
.
In the following example, we e show that t Pex x can n analyze e unsafe managed
.NETcode. We wrote the followingparameterizedunit test, that t obtains s an
unsafe pointer from a (safe) bytearray,thenpasses thepointer tothe .NET
UnmanagedMemoryStream
,whichisinturngiventothe
ResourceReader
.
[PexClass]
...
public partial class ResourceReaderTest t {
[PexMethod]
public unsafe void ReadEntriesFromUnmanagedMemoryStream(
[PexAssumeNotNull]byte[] data) {
fixed (byte* * p p = = data)
using (UnmanagedMemoryStream m stream m =
new UnmanagedMemoryStream(p, data.Length)) {
ResourceReader reader r =
new ResourceReader(stream);
readEntries(reader);
}
}
private static void readEntries(ResourceReader r reader) ) {
int i i = 0;
foreach (DictionaryEntry y entry y in n reader) ) {
PexAssert.IsNotNull(entry.Key);
i++;
}
}
}
Wefurtherdecoratethetestwiththefollowingattributes,tosuppresscertain
exceptionsthatthedocumentationdeemsacceptable,andtoenablePex’strict
checkingofunsafememoryaccesses.
[PexInjectExceptionsOnUnverifiableUnsafeMemoryAccess]
[PexAllowedException(typeof(BadImageFormatException))]
[PexAllowedException(typeof(IOException))]
[PexAllowedException(typeof(NotSupportedException))]
C# Image Convert: How to Convert Adobe PDF to Jpeg, Png, Bmp, &
String inputFilePath = @"C:\input.pdf"; String outputFilePath = @"C:\output.jpg"; // Convert PDF to jpg. C# sample code for PDF to jpg image conversion.
convert pdf to jpg; changing file from pdf to jpg
C# Image Convert: How to Convert Tiff Image to Jpeg, Png, Bmp, &
RasterEdge.XDoc.PDF.dll. C:\input.tif"; String outputDirectory = @"C:\output\"; // Convert tiff to jpg and show How to change Tiff image to Bmp image in your C#
to jpeg; convert pdf file to jpg file
Pex–WhiteBoxTestGenerationfor.NET
147
From the parameterizedunit test,Pex generates severaltest t inputs.After
aroundone minute,andexecutingtheparameterizedunit tests for 576 times
withdifferent inputs,Pexgenerates test-cases suchasthefollowing.(Mostof
thegeneratedtest-casesrepresentinvalidresourcefile,butsomerepresentlegal
resourcefileswithoneormoreentries.Thebytearrayshownhereisanillegal
resourcefile.)
public void ReadEntriesFromUnmanagedMemoryStream_576() {
byte[] bs0 0 = = new byte[56];
bs0[0] = (byte)206;
bs0[1] = (byte)202;
bs0[2] = (byte)239;
bs0[3] = (byte)190;
bs0[7] = (byte)64;
bs0[12] = = (byte)2;
bs0[16] = = (byte)2;
bs0[24] = = (byte)192;
bs0[25] = = (byte)203;
bs0[26] = = (byte)25;
bs0[27] = = (byte)176;
bs0[28] = = (byte)1;
bs0[29] = = (byte)145;
bs0[30] = = (byte)88;
bs0[40] = = (byte)34;
bs0[41] = = (byte)128;
bs0[42] = = (byte)132;
bs0[43] = = (byte)113;
bs0[44] = = (byte)132;
bs0[46] = = (byte)168;
bs0[47] = = (byte)5;
bs0[48] = = (byte)172;
bs0[49] = = (byte)32;
this.ReadEntriesFromUnmanagedMemoryStream(bs0);
}
Pexdeducedtheentirefilecontentsfromthe
ResourceReader
implementation.
Notethatthefirstfourbytesrepresentamagicnumberwhichthe
ResourceReader
expects.The later r bytes s form m resourceentries. The following code is s part t of
theresourcereaderimplementation.
ReadInt32
combinesfourbytestoa32-bit
integerthroughbitwiseoperations.
// Read d ResourceManager r header
// Check for r magic number
// _store e wraps s the input t stream
int magicNum = _store.ReadInt32();
if (magicNum m != = ResourceManager.MagicNumber)
throw new ArgumentException("Resource file not valid!");
JPG to PNG Converter | Convert JPEG to PNG, Convert PNG to JPG
Allow to change converting image with adjusted width & height; Change image resolution Open JPEG to PNG Converter first; Load JPG images from local folders in
convert pdf images to jpg; best pdf to jpg converter online
C# Create PDF from images Library to convert Jpeg, png images to
Batch convert PDF documents from multiple image formats, including Jpg, Png, Bmp, Gif, Tiff, Bitmap, .NET Graphics, and REImage.
bulk pdf to jpg converter; convert pdf pictures to jpg
148
N.TillmannandJ.deHalleux
5 Evaluation
WeappliedPexonacore.NETcomponentthathadalreadybeenextensively
testedoverseveralyears.
Weusedaversionofthecomponentwhichcontainsassertionchecksthatthe
developers of the component embeddedinto o the code. These checks arevery
expensive,andtheyareremovedfromtheretailversionofthecomponentthat
isnormallydeployedbytheusers.Theseadditionalconsistencychecks,realized
byconditionalbranchinstructions,greatlyincreasethenumberofpotentialex-
ecutionpathsthatmustbeanalyzed.Asaresult,Pexanalysistakesatleastan
orderofmagnitudelongerthanitdoeswhenappliedontheretailversion.
WeusedthePexWizardtogenerateindividualparameterizedunit testsfor
eachpublic method d of f all public classes.These automatically generatedunit
tests do o notcontainany additionalassertionvalidation; they simplypassthe
argumentsthroughtothemethod-under-test.Thus,thetestoracleonlyconsists
oftheassertionsthatareembeddedintheproductcode,andthepatternthat
certainexceptionsshouldnot bethrownbyany code,e.g.accessviolationex-
ceptionsthatindicatethat anunsafeoperationhas corruptedthememory.In
addition,wewroteabouttenparameterizedunit testsbyhandwhichexercise
commoncallsequences.
Forexample,foramethod
Parse
thatcreatesadatatype
DataType
instance
byparsingastring,theWizardgeneratesparameterizedunittestssuchasthe
following.
[PexMethod]
public void Parse(string s) ) {
DataType result t = DataType.Parse(s);
PexValue.AddForValidation("result", result);
}
The parameterized d unit test calls
DataType.Parse
with a given string and
storestheresultinalocalvariable.Thecallto
PexValue.AddForValidation
logs
theresultofthecallto
Parse
,anditthetestsuitewhichPexcreateswillinclude
verificationcodethatcanbeusedinfutureregressiontestingtoensurethatthe
Parse
willnotchangeitsbehaviorbutalwaysreturnthesameoutputaswhen
Pexexploredit.
We ranPex on n about t 10machines (different configurations,similar to o P4,
2GHz,2GBRAM) for threedays;eachmachinewas processingoneclassata
time.
Intotal,the analysis involvedmorethan10,000publicmethods withmore
than100,000blocksandmorethan100,000arcs.Whenexecutingthecodeas
partoftheanalysis,Pexcreatedasand-boxwithsecuritypermissions“Internet”,
i.e.permissionsthatcorrespondtothedefaultpolicypermissionsetsuitablefor
contentfromunknownorigin,whichmeans inparticularthatmost operations
involvingthe environment, e.g. file accesses, were blocked, Starting from the
publicmethods,Pexachievedabout43%blockcoverageand36%arccoverage.
Wedonotknowhowmanyblocksandarcsareactuallyreachable.
JPG to JBIG2 Converter | Convert JPEG to JBIG2, Convert JBIG2 to
Users may easily change image size, rotate image angle, set image rotation in dpi Covert JPG & JBIG2 image with high-quality; Provide user-friendly interface
convert .pdf to .jpg; convert pdf into jpg
VB.NET PDF Convert to Images SDK: Convert PDF to png, gif images
Convert PDF to Jpg, Png, Bmp, Gif, Tiff and Bitmap in ASP.NET. Or directly change PDF to Gif image file in VB.NET program with this demo code.
convert pdf file into jpg format; change format from pdf to jpg
Pex–WhiteBoxTestGenerationfor.NET
149
Table 1.Automaticallyachievedcoverageonselected classesof thecore.NET com-
ponent
Because of the restricted security permissions, , and the e fact that Pex was
only testing one method d at t atime, the overall coverage numbers clearly can
beimproved.However,Pexdidverywellonmanyclasseswhichdonotrequire
manymethodcalls toaccess their functionality. . Table 1 shows s a a selectionof
classesofthecore.NETcomponentonwhichPexfullyautomaticallyachieved
highblockandarccoverage.Onlylowerboundsfortheblockandarcnumbers
aregivenforproprietaryreasons.
OnecategoryoferrorsthatPexfoundcontainstestcasesthattriggerrather
benignexceptions,e.g.
NullReferenceException
and
IndexOutOfRangeException
.
Anothermoreinterestingcategoryof17uniqueerrorsinvolvestheviolationof
assertionswhichthedeveloperswroteinthecode,andtheexhaustionofmemory,
andotherseriousissues.
MostoftheerrorsthatPexfoundrequiredverycarefullychosenargumentval-
ues(e.g.astringoflength100filledwithparticularcharacters),anditisunlikely
thatarandomtestinputgeneratorwouldfindthem.Whilesomeoftheerrors
couldbefoundbyassertion-targettingtechniques,e.g.[18],thebranchconditions
thatguardedtheerrorswereusuallyquitecomplex (involvingbitvectorarith-
metic,indirectmemoryaccesses)andwerespreadovermultiplemethods,and
incorporatedvalues obtainedfromtheenvironment(here,theWindowsAPI).
Itrequiresadynamicanalysis(toobtainthevaluesfromtheenvironment)with
aprecisesymbolicabstractionoftheprogram’sbehaviortofindtheseerrors.
6 RelatedWork
Pex performspath-boundedmodel-checkingof.NETprograms.Pexis related
tootherprogrammodelcheckers,inparticularJPF[2]andXRT[14]whichalso
operateonmanagedprograms(Javaand.NET).BothJPFandXRThaveex-
tensionsforsymbolicexecution.However,bothcanonlyperformstaticsymbolic
execution,andtheycannotdealwithstatefulenvironmentinteractions.Also,in
the caseofJPF,onlysomeaspects of the programexecutioncanbe encoded
150
N.TillmannandJ.deHalleux
symbolically(linearintegerarithmeticconstraints),whileothersmustalwaysbe
exploredexplicitly(constraintsoverindirectmemoryaccesses).
Theideaofsymbolicexecutionwaspioneeredby[16].Laterworkondynamic
test generation,e.g.[17,18],mainly discussedthe generationoftest inputs to
determinewhether aparticular executionpathor branchwas feasible. . While
Pex’searchstrategiestrytoexerciseindividualexecutionpathsinaparticular
(heuristicallychosen)sequence,thestrategiesarecompleteandwilleventually
exerciseallexecutionpaths.Thisisimportantinanenvironmentsuchas.NET
wheretheprogramcanloadnew code dynamically,andnot t allbranches and
assertionsareknownaheadoftime.
DynamicsymbolicexecutionwasfirstsuggestedinDART[12].Theirtoolin-
strumentsCprogramsatthesourcecodelevel,andittrackslinearintegerarith-
meticconstraints.CUTE[27]followstheapproachofDART,butitcantrack
andreasonabout not only linearintegerarithmetic, but alsopointeraliasing
constraints.jCUTE[26]isanimplementationofCUTEforJava,amanageden-
vironmentwithoutpointers.EXE[6]isanotherimplementationofCsourcecode
baseddynamicsymbolicexecution,andEXEimplementsanumber of further
improvements,including constraint t caching, independent constraintoptimiza-
tion,bitvectorarithmetic,andtrackingindirectmemoryaccessessymbolically.
Eachof these approaches is specializedfor a particular source language,and
theyonlyincludecertainoperationsinthesymbolicanalysis.Also,theirsearch
orderisnot prioritizedtoachievehighcoveragequickly,whichforces theuser
topreciselydefineboundsonthesizeoftheprograminputsandtoperforman
exhaustivesearch.Pexislanguageindependent,anditcansymbolicallyreason
aboutpointerarithmeticaswellasconstraintsfromobjectorientedprograms.
Pex searchstrategies aim at t achievinghigh coverage e fast without muchuser
annotations.
AnotherlanguageagnostictoolisSAGE[13],whichisusedinternallyatMi-
crosoft.It virtualizes aWindows s process s onthe x86instructionlevel, , andit
tracksintegerconstraintsasbitvectors.Whileoperatingattheinstructionlevel
makesitaverygeneraltool,thisgeneralityalsocomeswithahighinstrumen-
tationoverheadwhichissignificantlysmallerforPex.
Severalimprovementshavebeenproposedrecentlytoimprovethescalability
ofdynamicsymbolicexecution,bymakingitcompositional[11,19],anddemand-
driven[19,8].WeareworkingonrelatedimprovementsinPex[1]withencour-
agingearlyresults.
Randoop[23]isatoolthatgeneratesnewtest-casesbycomposingpreviously
foundtest-casefragments,supplyingrandominputdata.Randoopwasalsoused
internallyinMicrosofttotestcore.NETcomponents.WhilePexandRandoop
foundsomeofthesameerrors,theerrorfindingsweregenerallydifferentinthat
Randoopfounderrorsthatneededtwoormoremethodcalls,whilemostofthe
errorsthatPexfoundinvolvedjustasinglemethodcalls,butwithverycarefully
chosenargumentvalues.
ThecommercialtoolAgitarOnefromAgitar[4]generatestest-casesforJava
by analyzing g the e source code, using information about program m invariants
Pex–WhiteBoxTestGenerationfor.NET
151
obtainedin a way y similar to o [9]. . Similar r to o idea of f parameterizedunit test-
ing[25],workbuildingonAgitarproposesaconceptcalledtheories[25]towrite
andexploregeneraltest-cases.
7 Conclusion
Pex[24]isanautomaticwhite-boxtestgenerationtoolfor.NETthatexplores
the code-under test t by y dynamic symbolic execution. Pexanalyzes safe,man-
agedcode,anditcanvalidateunsafememoryaccessesonindividualexecution
paths.WeappliedPexonaextremelywelltestedcore.NETcomponent,and
founderrors,includingaseriousissue.The automaticallyachievedresultsare
encouraging.However,thecombinedcoverageofthetest-casesthatPexgener-
atedfullyautomaticallyclearlyshowthatthereisroomforfutureresearch,e.g.
leveraginginformationaboutthestructureoftheprogramtoconstructmethod
callsequencesautomatically.
Acknowledgements
WewouldliketothankWolframSchulteforhissupport,ourinterns Thorsten
Schuett,ChristophCsallnerandSaswatAnandfortheirworktoimprovePex,
NikolajBjornerandLeonardodeMouraforZ3,thedevelopersandtestersofthe
core.NETcomponentfortheirsupportandadvice,aswellasPatriceGodefroid,
andtheanonymousreviewersfortheircomments.
References
1. Anand,S.,Godefroid, , P., Tillmann, N.: Demand-driven compositional symbolic
execution. Technical Report MSR-TR-2007-138, Microsoft Research, Redmond,
WA(October2007)
2. Anand,S.,Pasareanu,C.S.,Visser,W.:Jpf-se:Asymbolicexecutionextensionto
javapathfinder.In:Grumberg,O.,Huth,M.(eds.)TACAS2007.LNCS,vol.4424,
pp.134–138.Springer,Heidelberg(2007)
3. Bjorner,N.,deMoura,L.:Z3:AnefficientSMTsolver(2007),
http://research.microsoft.com/projects/Z3
4. Boshernitsan, , M., Doong, R., Savoia, , A.: : From daikon n to agitator: lessons and
challenges in building acommercial l tool for developer r testing. . In: ISSTA 2006:
Proceedingsofthe2006internationalsymposiumonSoftwaretestingandanalysis,
pp.169–180.ACMPress,NewYork(2006)
5. Brace,K.S.,Rudell,R.L.,Bryant,R.E.:EfficientimplementationofaBDDpack-
age. In: : DAC C 1990: Proceedings s of the 27th h ACM/IEEE E conference e on Design
automation,pp.40–45.ACMPress,NewYork(1990)
6. Cadar,C.,Ganesh,V.,Pawlowski,P.M.,Dill,D.L.,Engler,D.R.:Exe:automat-
ically generating g inputs s of f death. . In: CCS S 2006: Proceedings s of f the e 13th h ACM
conferenceon Computerand communications security,pp.322–335.ACMPress,
NewYork(2006)
152
N.TillmannandJ.deHalleux
7. Csallner, , C.,Tillmann, N., Smaragdakis, Y.:Dysy:Dynamicsymbolic execution
for invariantinference. TechnicalReport MSR-TR-2007-151, Microsoft Research,
Redmond,WA(November2007)
8. Engler,D.,Dunbar,D.:Under-constrainedexecution:makingautomaticcodede-
structioneasyandscalable.In:ISSTA2007:Proceedingsofthe2007international
symposiumonSoftwaretestingandanalysis,pp.1–4.ACM,NewYork(2007)
9. Ernst,M.D.,Perkins,J.H.,Guo,P.J.,McCamant,S.,Pacheco,C.,Tschantz,M.S.,
Xiao,C.:TheDaikonsystemfordynamicdetectionoflikelyinvariants.Scienceof
ComputerProgramming(2007)
10. Flanagan, , C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.:
ExtendedstaticcheckingforJava.In:Proc.theACMSIGPLAN2002Conference
onProgramminglanguage design andimplementation,pp.234–245.ACMPress,
NewYork(2002)
11. Godefroid,P.:Compositionaldynamictest t generation.In:POPL2007:Proceed-
ings of the 34th annual l ACM SIGPLAN-SIGACT T symposium on Principles of
programminglanguages,pp.47–54.ACMPress,NewYork(2007)
12. Godefroid,P.,Klarlund,N.,Sen,K.:DART:directedautomatedrandomtesting.
SIGPLANNotices40(6),213–223(2005)
13. Godefroid,P.,Levin,M.Y.,Molnar, , D.:Automated whiteboxfuzztesting.Tech-
nicalReportMSR-TR-2007-58,MicrosoftResearch,Redmond,WA(May2007)
14. Grieskamp,W., , Tillmann,N.,Schulte, W.:XRT-ExploringRuntimefor .NET
-Architectureand Applications.In:SoftMC 2005:Workshop on SoftwareModel
Checking,July2005.ElectronicNotesinTheoreticalComputerScience(2005)
15. E. . International. Standard ECMA-335, Common Language Infrastructure(CLI)
(June2006)
16. King,J.C.:Symbolicexecutionandprogramtesting.Commun.ACM19(7),385–
394(1976)
17. Korel,B.:Adynamicapproachof f testdatageneration.In:IEEEConferenceOn
SoftwareMaintenance,November1990,pp.311–317(1990)
18. Korel,B.,Al-Yami,A.M.:Assertion-orientedautomatedtestdatageneration.In:
Proc.the18thinternationalconferenceonSoftwareengineering,pp.71–80.IEEE
ComputerSociety,LosAlamitos(1996)
19. Majumdar, , R., Sen, K.: Latest: Lazy dynamic test t input t generation. Technical
ReportUCB/EECS-2007-36,EECSDepartment,UniversityofCalifornia,Berkeley
(Mar2007)
20. Two,M.C.,Poole,C.,Cansdale,J.,Feldman,G.,Newkirk,J.W.,Vorontsov,A.A.,
Craig,P.A.:NUnit,http://www.nunit.org/
21. Microsoft.Netframeworkgeneralreference-profiling(unmanagedapireference),
http://msdn2.microsoft.com/en-us/library/ms404386.aspx
22. Microsoft.VisualStudioTeamSystem,TeamEditionforTesters,
http://msdn2.microsoft.com/en-us/vsts2008/products/bb933754.aspx
23. Pacheco,C., , Lahiri,S.K., Ernst,M.D., Ball, T.: Feedback-directed random test
generation. In:ICSE 2007, Proceedings of the 29th International Conference on
SoftwareEngineering,Minneapolis,MN,USA,May23–25(2007)
24. Pexdevelopmentteam.Pex(2007),http://research.microsoft.com/Pex
25. Saff,D.,Boshernitsan,M.,Ernst,M.D.:Theoriesinpractice:Easy-to-writespeci-
ficationsthatcatchbugs.TechnicalReportMIT-CSAIL-TR-2008-002,MITCom-
puterScienceandArtificialIntelligenceLaboratory,Cambridge,MA,January14
(2008)
Pex–WhiteBoxTestGenerationfor.NET
153
26. Sen, , K., Agha, G.: CUTE and jCUTE: Concolic c unit t testing g and d explicit path
model-checkingtools.In:Ball,T.,Jones,R.B.(eds.)CAV2006.LNCS,vol.4144,
pp.419–423.Springer,Heidelberg(2006)
27. Sen, , K., Marinov, D., , Agha, , G.: Cute: a concolic unit testingengine for r c. . In:
ESEC/FSE-13:Proceedingsofthe10thEuropeansoftwareengineeringconference
held jointlywith 13th ACMSIGSOFT internationalsymposiumon Foundations
ofsoftwareengineering,pp.263–272.ACMPress,NewYork(2005)
28. Tillmann,N.,Schulte,W.:Parameterized d unittests.In:Proceedings of the10th
EuropeanSoftwareEngineeringConferenceheldjointlywith13thACMSIGSOFT
International Symposiumon Foundations of Software Engineering, pp.253–262.
ACM,NewYork(2005)
29. Tillmann, , N., Schulte,W.: Unit tests reloaded: Parameterized unit testing with
symbolicexecution.IEEESoftware23(4),38–47(2006)
Documents you may be interested
Documents you may be interested